Lars Frantzen  /  Publications

Here you find my papers and their BibTeX entries. See also my profile on Google Scholar.

[1] A. Bertolino, G. De Angelis, L. Frantzen, and A. Polini. The PLASTIC Framework and Tools for Testing Service-Oriented Applications. In A. De Lucia and F. Ferrucci, editors, Proceedings of the International Summer School on Software Engineering - ISSSE 2006-2008, number 5413 in Lecture Notes in Computer Science, pages 106-139. Springer, 2009. [ bib | .pdf ]
The emergence of the Service Oriented Architecture (SOA) is changing the way in which software applications are developed. A service oriented application consists of the dynamic composition of autonomous services independently developed by different organizations and deployed on heterogenous networks. Therefore, validation of SOA poses several new challenges, without offering any discount for the more traditional testing problems. In this chapter we overview the PLASTIC validation framework in which different techniques can be combined for the verification of both functional and extra-functional properties, spanning over both off-line and on-line testing stages. The former stage concerns development time testing, at which services are exercised in a simulated environment. The latter foresees the monitoring of a service live usage, to dynamically reveal possible deviations from the expected behaviour. Some techniques and tools which fit within the outlined framework are presented.

[2] L. Frantzen, M. N. Huerta, Z. G. Kiss, and T. Wallet. On-The-Fly Model-Based Testing of Web Services with Jambition. In R. Bruni and K. Wolf, editors, 5th International Workshop on Web Services and Formal Methods - WS-FM 2008, number 5387 in Lecture Notes in Computer Science, pages 143-157. Springer, 2009. [ bib | .pdf ]
Increasing complexity and massive use of current web services raise multiple issues for achieving adequate service validation while sticking to time-to-market imperatives. For instance: How to automate test case generation and execution for stateful web services? How to realistically simulate web service related operation calls? How to ensure conformance to specifications? The PLASTIC validation framework tackles some of these issues by providing specific tools for automated model-based functional testing. Based on the Symbolic Transition System model, test cases can be generated and executed on-the-fly. This testing approach was applied for validating the AlarmDispatcher eHealth service, aimed at providing health attention through mobile devices in B3G networks. In this paper we report how this modeling and testing approach helped to detect failures, support conformance, and reduce drastically the testing effort spent usually in designing test cases, validating test coverage, and executing test cases in traditional testing approaches.

[3] A. Bertolino, G. De Angelis, L. Frantzen, and A. Polini. Model-Based Generation of Testbeds for Web Services. In K. Suzuki et al., editor, Testing of Communicating Systems and Formal Approaches to Software Testing - TESTCOM/FATES 2008, number 5047 in Lecture Notes in Computer Science, pages 266-282. Springer, 2008. [ bib | .pdf ]
A Web Service is commonly not an independent software entity, but plays a role in some business process. Hence, it depends on the services provided by external Web Services, to provide its own service. While developing and testing a Web Service, such external services are not always available, or their usage comes along with unwanted side effects like, e.g., utilization fees or database modifications. We present a model-based approach to generate stubs for Web Services which respect both an extra-functional contract expressed via a Service Level Agreement (SLA), and a functional contract modeled via a state machine. These stubs allow a developer to set up a testbed over the target platform, in which the extra-functional and functional behavior of a Web Service under development can be tested before its publication.

[4] L. Frantzen and J. Tretmans. Model-Based Testing of Environmental Conformance of Components. In F.S. de Boer and M. Bonsangue, editors, Formal Methods of Components and Objects - FMCO 2006, number 4709 in Lecture Notes in Computer Science, pages 1-25. Springer, 2007. [ bib | .pdf ]
In component-based development, the correctness of a system depends on the correctness of the individual components and on their interactions. Model-based testing is a way of checking the correctness of a component by means of executing test cases that are systematically generated from a model of the component. This model should include the behaviour of how the component can be invoked, as well as how the component itself invokes other components. In many situations, however, only a model that specifies how others can use the component, is available. In this paper we present an approach for model-based testing of components where only these available models are used. Test cases for testing whether a component correctly reacts to invocations are generated from this model, whereas the test cases for testing whether a component correctly invokes other components, are generated from the models of these other components. A formal elaboration is given in the realm of labelled transition systems. This includes an implementation relation, called eco, which formally defines when a component is correct with respect to the components it uses, and a sound and exhaustive test generation algorithm for eco.

[5] L. Frantzen, J. Tretmans, and T.A.C. Willemse. A Symbolic Framework for Model-Based Testing. In K. Havelund, M. Núñez, G. Rosu, and B. Wolff, editors, Formal Approaches to Software Testing and Runtime Verification - FATES/RV 2006, number 4262 in Lecture Notes in Computer Science, pages 40-54. Springer, 2006. [ bib | .pdf ]
The starting point for Model-Based Testing is an implementation relation that formally defines when a formal model representing the System Under Test conforms to a formal model constituting its specification. An implementation relation for the formalism of Labelled Transition Systems is ioco. For ioco several test generation algorithms and test tools have been built. In this paper we define a framework for the symbolic implementation relation sioco which lifts ioco to Symbolic Transition Systems. These are transition systems with an explicit notion of data and data-dependent control flow. The introduction of symbolism avoids the state-space explosion during test generation, and it preserves the information present in data definitions and constraints for use during the test selection process. We show the soundness and completeness of the symbolic notions w.r.t. their underlying Labelled Transition Systems' counterparts.

[6] L. Frantzen, J. Tretmans, and R. d. Vries. Towards Model-Based Testing of Web Services. In A. Polini, editor, International Workshop on Web Services - Modeling and Testing - WS-MaTe 2006, pages 67-82, Palermo, Italy, 2006. [ bib | .pdf ]
Complex interactions between Web Services involve coordinated sequences of operations. Clients of the provided services must be aware of the underlying coordination protocol to smoothly participate in such a coordinated setup. In this paper we discuss on a running example how such protocols may also serve as the input for Model-Based Testing of Web Services. We propose to use Symbolic Transition Systems and the rich underlying testing theory to approach modelling and testing the coordination. We further indicate where theoretical and technical gaps exist and point to several research issues.

[7] A. Bertolino, L. Frantzen, A. Polini, and J. Tretmans. Audition of Web Services for Testing Conformance to Open Specified Protocols. In R. Reussner, J. Stafford, and C. Szyperski, editors, Architecting Systems with Trustworthy Components, number 3938 in Lecture Notes in Computer Science, pages 1-25. Springer, 2006. [ bib | .pdf ]
A Web Service (WS) is a type of component specifically conceived for distributed machine-to-machine interaction. Interoperability between WSs involves both data and messages exchanged and protocols of usage, and is pursued via the establishment of standard specifications to which service providers must conform. In previous work we have envisaged a framework for WS testing. Within this framework, this paper focuses on how the intended protocol of access for a standard service could be specified, and especially on how the conformance of a service instance to this specified protocol can then be tested. We propose to augment the WSDL description with a UML2.0 Protocol State Machine (PSM) diagram. The PSM is intended to express how, and under which conditions, the service provided by a component through its ports and interfaces can be accessed by a client. We then propose to translate the PSM to a Symbolic Transition System, to which existing formal testing theory and tools can be readily applied for conformance evaluation. A simple example illustrates the approach and highlights the peculiar challenges raised by WS conformance testing.

[8] A. v. Weelden, M. Oostdijk, L. Frantzen, P. Koopman, and J. Tretmans. On-the-Fly Formal Testing of a Smart Card Applet. In R. Sasaki, S. Qing, E. Okamoto, and H. Yoshiura, editors, 20th IFIP International Information Security Conference - SEC 2005, pages 564-576. Springer, 2005. [ bib | .pdf ]
This paper presents a case study on the use of formal methods in specification-based, black-box testing of a smart card applet. The system under test is a simple electronic purse application running on a Java Card platform. The specification of the applet is given as a Statechart model, and transformed into a functional form to serve as the input for the on-the-fly test generation, -execution, and -analysis tool GAST. We show that automated, formal, specification-based testing of smart card applets is of high value, and that errors can be detected using this model-based testing.

[9] A. Belinfante, L. Frantzen, and C. Schallhart. Model-Based Testing of Reactive Systems, chapter Tools for Test Case Generation, pages 391-438. Number 3472 in Lecture Notes in Computer Science. Springer, 2005. [ bib | .pdf ]
In this chapter we will present a selection of model-based test tools which are (partly) based on the theory discussed in the preceding chapters. After a general introduction of every single tool we will hint at some papers which try to find a fair comparison of some of them.

[10] L. Frantzen, J. Tretmans, and T.A.C. Willemse. Test Generation Based on Symbolic Specifications. In J. Grabowski and B. Nielsen, editors, Formal Approaches to Software Testing - FATES 2004, number 3395 in Lecture Notes in Computer Science, pages 1-15. Springer, 2005. [ bib | .pdf ]
Classical state-oriented testing approaches are based on simple machine models such as Labelled Transition Systems (LTSs), in which data is represented by concrete values. To implement these theories, data types which have infinite universes have to be cut down to finite variants, which are subsequently enumerated to fit in the model. This leads to an explosion of the state space. Moreover, exploiting the syntactical and/or semantical information of the involved data types is non-trivial after enumeration. To overcome these problems, we lift the family of testing relations ioco to the level of Symbolic Transition Systems (STSs). We present an algorithm based on STSs, which generates and executes tests on-the-fly on a given system. It is sound and complete for the ioco testing relations.

[11] A. v. Weelden, M. Oostdijk, L. Frantzen, P. Koopman, and J. Tretmans. On-the-Fly Formal Testing of a Smart Card Applet. Technical Report NIII-R0428, Radboud University Nijmegen, June 2004. This is a preliminary technical report of [8]. [ bib | .pdf ]
[12] L. Frantzen. Approaches for Analysing and Comparing Packet Filtering in Firewalls. Master's thesis, Technical University of Berlin, 2003. [ bib | .pdf ]
[13] L. Frantzen, J. Tenzer, D. Parnitzke, M. Piirainen, M. Klein, A. Simon, U. Wagner, and B. Braatz. From Algebraic Module Specifications to Component Concepts and Integrated Modeling Techniques. Technical Report 2001/21, Technical University of Berlin, 2001. [ bib | .ps.gz ]

This file was generated by bibtex2html 1.96.