Tutorials

Invited Talks (More talks will be announced)

Abstracts

• Communications Protocol System Testing: Theory and Applications
  ===============================================================
  David Lee
  The Ohio State University, Department of Computer Science & Engineering. Ohio, USA
  
  After a description of the finite state machine formalism and on how to test these machines, the fundamental theory is illustrated with examples and applications in communication protocol system analysis. Taking as starting point the the basic theory, a few new topics are discussed, including:
  (1) IP protocol testing;
  (2) Network passive monitoring;
  (3) Integrated system interoperability testing; and
  (4) Security protocol testing;

• Model-based Testing and Validation of Real-Time Systems
  ======================================================
  Kim Guldstrand Larsen
  CISS, Aalborg University, Denmark
  with
  Brian Nielsen
  CISS, Aalborg University, Denmark
  
  These lectures will give provide a thorough tutorial of the tool UPPAAL and the newly emerged branches UPPAAL Tron, UPPAAL Cora and UPPAAL Tiga (see www.uppaal.com) and their application to the modelling, simulation, verification, testing, scheduling and controller synthesis for real time and embedded systems.
  
  UPPAAL is a tool for modelling, simulating and verifying real-time systems, developed as a collaboration between BRICS at Aalborg University and Department of Computer Systems at Uppsala University since the beginning of 1995.  The modelling language of UPPAAL is based on the notion of timed automata by Alur and Dill (1990) allowing system behaviour to be described as a networks of timed automata extended with data variables which may be manipulated by a rich C-like programming language. UPPAAL includes a similator for inexpensive validation of behaviour and a verifier for model-checking wrt safetly, liveness and bounded liveness properties. The newly released UPPAAL 4.0 offers a number of improvements and extension, including symmetry reduction, user defined functions, priorities on processes and channels, new abstraction techniques, a factor 3 to 5 reduction in memory usage, fully searchable help system, implementation of generalized sweep line method, record types, quantifiers in expressions, undo and redo support, syntax highlighting, custom location and edge colors, documentation comments on models and better trace facilities.
  
  UPPAAL Tron is a testing tool, based on the UPPAAL engine, allowing for on-line conformance testing of timed systems, mainly targeted for embedded software commonly found in various controllers. By on-line we mean that tests are derived, executed and checked simultaneously while maintaining the connection to the system in real-time.  UPPAAL Tron
  
  UPPAAL Cora is a branch of UPPAAL targeted towards optimal scheduling and planning problems with numerous applications to embedded systems.
  The modelling formalism of UPPAAL Cora is that of priced timed automata - an extension of the classical timed automata model - allowing models to be annotated with information describing how various types of costs and rewards (e.g. energy, throughput) may accumulate during the behaviour of a model.
  
  UPPAAL Tiga is the most recent branch of UPPAAL supporting controller synthesis for real time systems through the computation of winning strategies for timed games.
  
  Both UPPAAL Cora and UPPAAL Tiga allows for efficient off-line generation of (cost-wise) optimal test-suites with guaranteed coverage.

• The Why, What and How of (not) software testing
  =============================================
  Antonia Bertolino
  Istituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo", CNR, Pisa, Italy
  
  This talk will provide a broad overview of software testing basic concepts and the various proposed techniques, spanning over white-box and black-box approaches, and highlighting the different assumptions behind them. We will illustrate for instance the difference between testing for debugging and testing for reliability. Goal of the talk is to evidence the strict dependence of the effectiveness of any adopted technique from the pursued test objective. A critical attitude towards any "packed" solution to software testing must therefore be matured for the highest efficacy.

• Systems Validation and Verification at Airbus
  =========================================
  Odile Lauren
  EYDT (Methods and tools) Airbus France
  
  With the growing size and complexity of embedded systems, verification and validation activities are becoming a real challenge, especially for critical real-time systems. This talk will give an overview of the validation and verification process for systems at Airbus. The different steps of the testing process will be shown all along the system development life cycle from the system specification up to the system integration into the aircraft. The link between the system specification phase and the testing process will be highlighted. In particular, the use of formal methods for specifying systems and its consequences on the verification and validation process will be explained. Moreover, the impacts of the certification constraints will be discussed. As Airbus has used formal methods for several years to specify avionics systems and automatically generates code from formal specifications, new perspectives for testing process are possible. Indeed, some verification activities that are led today at code level, could be conducted at model level in order to demonstrate the system specifications meet the system requirements. This possible new approach will be briefly tackled.
  
• Specification-Based Testing of Synchronous Software
  ==================================================
  Ioannis Parissis
  Université Joseph Fourier - LSR-IMAG, Grenoble, France

  Synchronous software satisfies the synchrony hypothesis which states that every reaction of the software to its inputs is theoretically instantaneous and deterministic. Dedicated programming languages have been designed for specifying and programming synchronous software; Lustre is one of them.

  The verification and validation of synchronous programs specified in Lustre has been in the center of several investigations that have focused on fully automated proof by model-checking or on automated testing.

  This presentation is concerned with testing automation of synchronous software specified in Lustre and the Lutess environment, developed at LSR-IMAG laboratory. Lutess offers several specification-based black-box testing techniques which are variations of constrained random testing . The specification of the environment of the software (that is, of the external event sequences that the software must process) is automatically transformed into a random test data generator which interacts with the software and, at every cycle of the software execution, computes the set of valid software input values and issues a randomly selected value among them.

  Through constrained random testing one gets a way, for instance, to assess software reliability since the generation process can take into account the specification of operational profiles. Another variation of constrained random testing supported by Lutess is safety-property-guided generation: it consists in automatically analyzing the specification of the safety properties and modifying the constrained random generator so that it preferably sends out test data sequences which adequately test the software safety.

  The presentation will address the following points:

  1. Brief introduction to synchronous programming and the Lustre language
  2. Overview of the main verification approaches for Lustre specifications and programs
  3. Presentation of the Lutess testing environment
     •  Formal foundations
     •  Implementation details
     •  Short tool presentation (Lutess will be available during the TAROT lab sessions).
     •  Work in progress

   

	TAROT SUMMER SCHOOL 2006.