Lars Frantzen  /  Publications  /  BibTeX
  author = {A. Bertolino and G. De Angelis and L. Frantzen and A. Polini},
  title = {{The PLASTIC Framework and Tools for Testing Service-Oriented Applications}},
  booktitle = {Proceedings of the International Summer School on Software Engineering -- ISSSE 2006-2008},
  year = {2009},
  editor = {A. De Lucia and F. Ferrucci},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  number = {5413},
  pages = {106--139},
  url = {},
  abstract = {
  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
  author = {L. Frantzen and M. N. Huerta and Z. G. Kiss and T. Wallet},
  title = {{On-The-Fly Model-Based Testing of Web Services with Jambition}},
  booktitle = {5th International Workshop on Web Services and Formal Methods -- WS-FM 2008},
  year = {2009},
  editor = {R. Bruni and K. Wolf},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  number = {5387},
  pages = {143--157},
  url = {},
  abstract = {
  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.
  author = {A. Bertolino and G. De Angelis and L. Frantzen and A. Polini},
  title = {{Model-Based Generation of Testbeds for Web Services}},
  booktitle = {Testing of Communicating Systems and Formal Approaches to Software Testing -- TESTCOM/FATES 2008},
  year = {2008},
  series = {Lecture Notes in Computer Science},
  number = {5047},
  pages = {266--282},
  editor = {K. Suzuki et al.},
  publisher = {Springer},
  url = {},
  abstract = {
  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.
  author = {Frantzen, L. and Tretmans, J.},
  title = {{Model-Based Testing of Environmental Conformance
           of Components}},
  booktitle = {{Formal Methods of Components and Objects -- FMCO 2006}},
  editor = {Boer, F.S. de and Bonsangue, M.},
  year = {2007},
  pages = {1--25},
  series = {Lecture Notes in Computer Science},
  number = {4709},
  url = {},
  publisher = {Springer},
  abstract = {
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.
  author = {L. Frantzen and J. Tretmans and T.A.C. Willemse},
  title = {{A Symbolic Framework for Model-Based Testing}},
  booktitle = {Formal Approaches to Software Testing and Runtime Verification -- FATES/RV 2006},
  year = {2006},
  editor = {K. Havelund and M. N{\'u}{\~n}ez and G. Rosu and B. Wolff},
  number = {4262},
  series = {Lecture Notes in Computer Science},
  pages = {40-54},
  publisher = {Springer},
  url = {},
  abstract = {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'
  author = {L. Frantzen and J. Tretmans and R. d. Vries},
  title = {{Towards Model-Based Testing of Web Services}},
  booktitle = {International Workshop on Web Services - Modeling and Testing -- WS-MaTe 2006},
  pages = {67-82},
  year = {2006},
  editor = {A. Polini},
  address = {Palermo, Italy},
  url = {},
  abstract = {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.}
  author = {A. Bertolino and L. Frantzen and  A. Polini and J. Tretmans},
  title = {{Audition of Web Services for Testing Conformance to Open Specified Protocols}},
  booktitle = {Architecting Systems with Trustworthy Components},
  year = {2006},
  editor = {R. Reussner and J. Stafford and C. Szyperski},
  number = {3938},
  series = {Lecture Notes in Computer Science},
  pages = {1-25},
  publisher = {Springer},
  url = {},
  abstract = {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.}
  author = {A. v. Weelden and M. Oostdijk and L. Frantzen and P. Koopman and J. Tretmans},
  title = {{On-the-Fly Formal Testing of a Smart Card Applet}},
  booktitle = {20th IFIP International Information Security Conference -- SEC 2005},
  editor = {R. Sasaki and S. Qing and E. Okamoto and H. Yoshiura},
  pages = {564--576},
  publisher = {Springer},
  year = 2005,
  isbn = {0-387-25658-X},
  url = {},
  abstract = {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.}
  author = {A. Belinfante and L. Frantzen and C. Schallhart},
  chapter = {Tools for Test Case Generation},
  title = {{Model-Based Testing of Reactive Systems}},
  publisher = {Springer},
  year = {2005},
  pages = {391-438},
  number = {3472},
  series = {Lecture Notes in Computer Science},
  url = {},
  abstract = {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.}
  author = {L. Frantzen and J. Tretmans and T.A.C. Willemse},
  title = {{Test Generation Based on Symbolic Specifications}},
  booktitle = { Formal Approaches to Software Testing -- FATES 2004},
  pages = {1-15},
  year = {2005},
  editor = {J. Grabowski and B. Nielsen},
  number = {3395},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  url = {},
  abstract = {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.}
  author = {A. v. Weelden and M. Oostdijk and L. Frantzen and P. Koopman and J. Tretmans},
  title = {{On-the-Fly Formal Testing of a Smart Card Applet}},
  institution = {Radboud University Nijmegen},
  year = {2004},
  number = {NIII-R0428},
  month = {June},
  url = {},
  note = {This is a preliminary technical report of \cite{vWOF+05}}
  author = {L. Frantzen},
  title = {{Approaches for Analysing and Comparing Packet Filtering in Firewalls}},
  school = {Technical University of Berlin},
  year = {2003},
  url = {}
  author = {L. Frantzen and J. Tenzer and D. Parnitzke and M. Piirainen and M. Klein and A. Simon and U. Wagner and B. Braatz},
  editor = {H. Ehrig},
  title = {{From Algebraic Module Specifications to Component Concepts and Integrated Modeling Techniques}},
  institution = {Technical University of Berlin},
  year = {2001},
  number = {2001/21},
  url = {}

This file was generated by bibtex2html 1.96.