August 26th to 29th, 2002
Testing based on Finite State Machines, A. Petrenko
Software Model Checking, G. Holzman
Synthesis of Communication Systems, G. v. Bochmann
Testing and Test Control Notation (TTCN-3), I. Schieferdecker
Techniques for Deriving Performance Models from Software Designs, M. Woodside
Feature Interactions, L. Logrippo
Distributed Feature Composition, P. Zave
SDL Design Patterns, R. Gotzhein
User Requirements Notation, D. Amyot
A. Petrenko
CRIM
In the context of software engineering, Finite State Machines, FSMs, are ubiquitously used from the requirement engineering, to testing and documentation. The talk focuses on the testing problems formulated in terms of FSM with a special attention to fault detection. In this setting, one usually assumes that the specification of the expected behavior of a system under test is given as a FSM and needs to derive tests such that implementation faults of interest could be detected.
The model of FSM is simple, intuitive, and easy to apply, at the same time, there are numerous types and variations of state machines that emphasize different aspects of systems and thus require different methods for their manipulations. In this talk, we recall basic definitions of classical input/output FSMs, provide their categorization, and define key concepts, such a conformance relation, related to testing issues.
We introduce a basic testing framework based on FSM and analyze main testing assumptions used in this framework. One of important elements of this framework is the notion of a fault model that is defined as a triple, an FSM specification, implementation domain and conformance relation, where the implementation domain is a set of potential implementations that reflects the test assumptions. We provide several typical fault models used in FSM testing. Based on a fault model, the notion of a complete test suite (checking experiment) is introduced as a set of tests that guarantee detection of any implementation FSM from the given implementation domain that does not conform to the specification FSM for a given conformance relation.
We present the classical methods for deriving complete test suites from a completely defined reduced deterministic FSM and explain the underlying ideas using examples, so that the listeners could learn them during the lecture. Then we discuss other important classes of FSMs such as partially defined, non-reduced and nondeterministic machines and discuss appropriate methods for deriving tests. In the final part of the talk, we overview various extensions to the basic FSM model, communicating FSMs (CFSM), Extended FSM (EFSM) and test derivation issues they pose. We conclude by providing a snapshot of the ongoing research in the field and stating few unsolved testing problems.
Alexandre Petrenko received his Ph.D. degree in Computer Science from the Institute of Electronics and Computer Science, Riga, USSR. In 1996, he has joined CRIM, Centre de Recherche Informatique de Montréal, Canada, as a Senior Researcher. From 1992 to 1996, he was a visiting professor/researcher of the Université de Montréal. From 1982 to 1992, he was the head of a research department of the Institute of Electronics and Computer Science in Riga. From 1979 to 1982, he worked in the International Institute for Applied Systems Analysis (IIASA), Vienna, Austria. He also had visiting research positions at Politecnico di Milano and Universita di Catania in Italy; University of Osaka in Japan; R&D Center of Siemens AG in Germany; France Telecom R-D, Lannion; and University of Sao Paulo in Sao Carlos in Brazil. A. Petrenko is a member of the Steering Committee of the IFIP conference on Testing Communicating Systems (TestCom) and serves in the Program Committee for several other conferences. He has published over 150 papers and has been involved in numerous research projects related to testing problems.
Gerard J. Holzmann
Bell-Labs
We will discuss the challenge and the promise of software model checking techniques. Doing so, we will focus primarily on SPIN: a widely used logic model checking tool for asynchronous process systems. SPIN is specifically designed for handling software rather than hardware applications. The tool can handle verification problems that would ordinarily remain well beyond the scope of software analysis tools with proof approximation techniques.
We will review the automata theoretic verification method for on-the-fly LTL model checking on which SPIN is founded, and we will review some of the algorithms that make SPIN particularly efficient. We will also discuss some significant recent applications of software model checking, e.g., the applications done at NASA in flight software verification and at Lucent in the verification of industrial call processing software. We conclude with a review of a promising new technique for mechanically extracting SPIN verification models from implementation level ANSI-C software.
Gerard J. Holzmann received his PhD in Technical Sciences from the Delf University of Technology in The Netherlands in 1979. He first joined the Computing Sciences Research group at Bell Labs in 1980 where he is currently Director of the Computing Principles Research Department. He was the recipient of the 2001 ACM System Software Award and the 2002 ACM SIGSOFT Outstanding Research Award for his design of the SPIN model checker. He has written three books, authored over 70 technical papers, and holds seven U.S. Patents in verification and in image processing.
Dr.-Ing. Ina Schieferdecker
FOKUS
Fraunhofer Institute for Open Communication Systems
Kaiserin-Augusta-Allee 31, D-10589 Berlin, Germany
Phone: +49-30-3463 7241, Fax: +49-30-3463 8241
e-mail: schieferdecker@fokus.fhg.de
In system engineering, testing is a generally accepted approach to validate systems and system components. Assured quality of system and system components is particularly important, as the time-to-market become ever shorter. A systematic approach to testing distributed systems is essential, so that the requirements of the market can be fulfilled. The Testing and Test Control Notation TTCN-3, being the third edition of TTCN, has been developed by ETSI to address testing needs of modern telecom and datacom technologies. TTCN-3 is not restricted to conformance testing and can be used for many other kinds of testing including interoperability, robustness, regression, system and integration testing. Typical areas of application are protocol testing (including mobile and Internet protocols), service testing (including supplementary services), module testing, testing of CORBA based platforms, API testing etc. It also enables systematic, specification-based testing for software systems based e.g. on CORBA, EJB or XML technologies.
TTCN-3 is the only standardised language for the specification and implementation of test cases. It has been developed to support black-box testing on the basis of behavioural interface specifications of a system under test (SUT). TTCN-3 allows an easy and efficient description of complex distributed test behaviour. It is a modular language and has a similar look and feel to a typical programming language. Besides typical programming constructs, it contains all the important features necessary to specify test procedures and campaigns. In addition to the pure textual format, the Tabular Presentation Format for TTCN-3 (TFT) and the Graphical Presentation Format for TTCN-3 (GFT) have been defined to provide a graphical means both for the data and the behaviour aspects.
TTCN-3 is on syntactical (and methodological) level a drastic change compared to previous TTCN versions. However, the main concepts of TTCN have been retained and improved and new concepts have been included, so that TTCN-3 is applicable for a broader class of systems. New concepts are, e.g. a test execution control program to describe relations between test cases such as sequences, repetitions and dependencies on test outcomes, dynamic concurrent test configurations, and test behaviour in asynchronous and synchronous communication environments. Further improved concepts are, e.g. the integration of ASN.1, the module and grouping concepts to improve the test suite structure, and the test component concepts to describe concurrent test setups.
Outline
This lecture on "TTCN-3 - The Testing and Test Control Notation" will cover the following topics:
Related Papers
Further Material
Dr.-Ing. Ina Schieferdecker studied mathematical computer science at the Humboldt University in Berlin and received her Ph.D. on Performance-Enhanced System Specifications from the Technical University in Berlin in 1994. She attended the postgraduate course on open communication systems at the Technical University in Berlin. Since 1993, she is a researcher at GMD FOKUS, now Fraunhofer FOKUS and a lecturer at Technical University Berlin since 1995. In 1997, she had a research stay at the International Computer Science Institute, Berkeley, California working on test concepts for IP Telephony Systems.
Her technical and research work covers testing methods for distributed systems and formal methods for the design, validation and prototyping of distributed systems. Ina Schieferdecker is the head of the Competence Center for Testing, Interoperability and Performance (TIP) since 1997. Ina Schieferdecker is actively involved in several R&D projects on testing being responsible for developing test concepts, designing and implementing test systems as well as performing test campaigns. She wrote research papers on various aspects of testing distributed systems and of developing test systems.She is involved in the definition of MSC at ITU-T SG10 and of TTCN-3 at ETSI, in particular in the graphical presentation format of TTCN-3. She initiated the work on the UML testing profile at OMG and is coordinating the work thereof.
Murray Woodside
Carleton University
To support the use of performance analysis in early stages of software development, predictive models must be made based on software requirements, architecture, and designs. Annotations to designs, and systematic methods (or even automated tools) for model creation, are needed. Performance parameters have to be estimated or budgeted.
Completions representing system infrastructure must be introduced. The presentations will describe approaches that lead to layered queueing models of performance, and experience with telecommunications products.
Murray Woodside has taught and done research in stochastic control, optimization, queuing theory, and performance modeling of communications and computer systems, with over 100 articles in these subjects. His current interests are software engineering and performance engineering of distributed systems and telecommunications software. He invented the layered queueing model for software performance in 1984, and has contributed heavily to its development. He currently holds the OCRI/NSERC Industrial Research Chair in Performance Engineering of Real-Time Software at Carleton University, where he has taught since 1970. He is one of the founders of the International Workshop on Software and Performance (WOSP).
Luigi Logrippo
SITE, University of Ottawa
Telecommunications systems offer not only basic connectivity, but also the ability to be programmed to provide value-added features. Traditional standard features such as Call Forward, Call Screening, and Call Waiting are well known. However, with the advent of internet telephony, every device in a network can be programmed, by the user or by the utility, to provide arbitrarily complex features.
Pamela Zave
AT&T Laboratories
Distributed Feature Composition (DFC) is a virtual architecture for the description of telecommunication services. It was designed for generality, feature modularity, structured feature composition, and analysis of feature interactions.
After giving an overview of DFC, I will cover two DFC topics in more depth:
(1) AT&T's IP implementation of DFC, with an emphasis on how we optimize media transmission while retaining feature modularity.
(2) Guidelines for creating new, IP-enabled telecommunication services, with an emphasis on a systematic approach to feature interactions caused by address translation.
Pamela Zave received the A.B. degree in English from Cornell University, Ithaca, New York, and the Ph.D. degree in computer sciences from the University of Wisconsin--Madison. She began her career as an Assistant Professor of Computer Science at the University of Maryland, College Park. Since 1981 she has been with AT&T Research, and is now a Technology Advisor in the Network Services Research Laboratory.
Dr. Zave has approximately 70 publications, of which "A Compositional Approach to Multiparadigm Programming" won the Best Paper of 1989 award from IEEE Software. She also has two patents and two patents pending in the telecommunication area. She has given numerous talks all over the world, including invited lectures at 20 conferences. She is a member of IFIP Working Group 2.3 (Programming Methodology) and IFIP Working Group 2.9 (Requirements Engineering).
Dr. Zave is an associate editor of Requirements Engineering, a former associate editor of IEEE Transactions on Software Engineering, a former associate editor of ACM Computing Surveys, and a former officer of the ACM Special Interest Group on Software Engineering. She served as a guest editor of the January 1986 special issue of IEEE Transactions on Software Engineering on software design methods. She has served on the program committees of many conferences, including chairing the program committee of the Second IEEE International Symposium on Requirements Engineering, and co-chairing the program committee of Formal Methods Europe 2001.
Reinhard Gotzhein
Computer Networks Group
University of Kaiserslautern, Germany
Design Patterns have evolved into a well-established reuse approach in software engineering. A design pattern is a generic solution for a recurring design problem, which is selected from a pattern pool, adapted and finally composed with a design description. Design patterns raise the vocabulary of system engineers to a problem-oriented level, assist the exploitation of commonalities, and lead to high-quality, well-justified system designs. The Computer Networks Group at the University of Kaiserslautern has advanced the pattern idea by combining it with the formal design language SDL, yielding the SDL-pattern approach. SDL (Specification and Description Technique) is one of the few formal description techniques that are widely used in industry. One reason for this success is certainly the graphical notation, which supports the intuitive understanding of specifications. Furthermore, the availability of excellent commercial tool environments has contributed to the wide distribution of SDL in industry. The SDL-pattern approach consists of the SDL-pattern design process, a notation for the description of generic SDL fragments called PA-SDL (Pattern Annotated SDL), a template and rules for the definition of SDL patterns, and an SDL-pattern pool for the communication systems domain. The approach has been applied successfully to the engineering and re-engineering of several communication systems, including the Internet Stream Protocol ST2+, a quality-of-service management and application functionality for CAN (Controller Area Network), and the customized communication system of the light control in a building. By now, the SDL-approach can be assessed as being consolidated, transfer to the telecommunications industry (e.g., for the engineering of UMTS-protocols) is on the way.
Contents of the lecture:
Lecture material:
Participants will receive paper copies of the lecture material, and electronic copies of the case study and all SDL-patterns that are applied in the case study.
Intended audience:
Reinhard Gotzhein received his Diploma (M.Sc.) and Dr.-Ing. (Ph.D.) degrees in computer science from the University of Erlangen, Germany, in 1982 and 1985, respectively. From 1985 until 1986, he was a post-doctoral fellow at the University of Montreal, Canada. From 1987 until 1993, he worked as Assistant Professor at the University of Hamburg, Germany, where he also completed his Habilitation in 1992. From 1991 until 1992, he was a visiting professor at the University of Montreal. Since 1993, he is an Associate Professor at the University of Kaiserslautern, heading the Computer Networks Group. His research interests include communication systems, protocol engineering, software reuse technologies, and formal description techniques. Dr.
Gotzhein has published more than 100 scientific papers. Since 1998, he is acting as Associate Rapporteur of the ITU-T on the semantics of SDL. He chaired the FORTE/PSTV’96 International Conference, has served on program committees for numerous international symposia, as guest editor for several scientific journals, and as scientific advisor of a research institute.
Daniel Amyot
SITE, University of Ottawa
Requirements engineering has become an essential part of the development of complex software and systems in general. However, very few standardized notations and techniques exist to address practical issues related to the visualization and understanding of functional and non-functional requirements. The User Requirements Notation (URN), which will become an ITU-T standard by the end of 2003, represents one of the first attempts at standardizing a requirements notation for complex dynamic systems such as e-commerce applications, telecommunication systems, and other types of reactive and distributed systems.
This tutorial will present the motivations behind URN, its objectives, and the current proposal that combines two complementary languages. The first one, GRL (Goal-oriented Requirement Language), is used to describe business goals, non-functional requirements, alternatives, and rationales. The second one, UCM (Use Case Maps), enables the description of functional requirements as causal scenarios. The tutorial will provide an introduction to both languages, with illustrative examples and tool support. Several advanced concepts and applications will also be covered: generation of MSC from UCMs, validation of UCM specifications, and relationships between UCM and GRL, between URN and UML, and between URN and other languages standardized by ITU-T. The tutorial will also include an interactive exercise.
Daniel Amyot recently joined SITE (University of Ottawa) as an Assistant Professor, after working 18 months as a senior researcher in the telecommunication industry. Daniel has several years of teaching experience in academic and industrial settings. He has been working extensively with UCMs for the last nine years and is in charge of the Use Case Maps Users Group. He is also the ITU-T Rapporteur on the User Requirements Notation and chairs the URN Focus Group. He holds a Ph.D. (Specification and Validation of Telecommunications Systems with Use Case Maps and LOTOS) and a M.Sc. from the University of Ottawa (2001 and 1994), as well as a B.Sc. from Laval University (1992). Daniel published many papers on UCMs and URN, and he presented tutorials on the UCM notation at ICSE'01, ISRE'01 and UML'01.
Rachida Dssouli, Ferhat Khendek, and Thiruvengadam Radhakrishnan
Concordia University
| First Name: | |
| Last Name: | |
| Position: | |
| Department: | |
| University/Company/Organization: | |
| Address: | |
| City: | |
| Province/State: | |
| Country: | |
| Postal/Zip Code: | |
| Telephone: | |
| Fax: | |
| E-mail: |
| Before June 30th, 2002 | After June 30th, 2002 | |
| Students | 150$ | 200$ |
| Regular participants | 300$ | 400$ |
| (Includes participant proceedings, lunches and coffee breaks.) | ||
| Cheque/Money Order, or cash on the site (Please make Cheques/Money Orders payable to Concordia University) |
| Rachida Dssouli, Professor | |
| dssouli@ece.concordia.ca | |
| Office H-961-43 | |
| Electrical and Computer Engineering Dept | Tel/Ph: 514-848-4162 |
| Concordia University | Fax: 514-848-2802 |
| 1455 de Maisonneuve Blvd, West | |
| Montreal, Quebec | |
| Canada H3G 1M8 |