- Alexandre Petrenko, CRIM, Canada (supported by Formal Methods Europe)
Some Observations on Progress in Formal Methods for Testing
In this invited talk devoted to the 25th anniversary of the ICTSS, we discuss the advancements in Formal Methods for Model Based Testing (MBT) during this period. A number of research problems chosen for discussions include the variety of formal models, challenges in using these models, nondeterminism, fault models and others.
- Ana R. Cavalli, Telecom SudParis, France
From active testing to monitoring techniques. Application to test secure interoperability.
Conformance testing techniques are used to check if a given system implementation satisfies its specification or some predefined properties. These testing techniques can be active, based on the execution of specific test sequences against the implementation under test, or passive, based on the observation of the exchange of messages (input and output events) of the implementation under test during run-time. In the last years an important research activity has taken place dealing with monitoring techniques based on passive testing.
In this talk, we will present the evolution of these testing techniques, their advantages and limitations. We will also illustrate their application to the security testing of real case studies. In particular, we will illustrate the application of the monitoring techniques to test the secure interoperability of a Multisource Information System. Security and interoperability have been identified as essential by researchers, developers, users and operators of systems and networks.
- Jens Herrmann, Daimler AG, Germany
ARTEMIS Project MBAT: Combining Model-based Testing and Static Analysis to Improve Quality and Reduce Efforts
MBAT is an strongly industrial-oriented 3-years ARTEMIS R&D project comprising 39 partners from 8 European countries which has started in 2011 (more info here: http://www.mbat-artemis.eu). MBAT will provide European industry with a new leading-edge technology which allows to develop high-quality & safe embedded systems at reduced costs in terms of time and money, focusing on Validation & Verification (V&V) of embedded systems used in the transportation domain (automotive, aerospace, rail). The increased V&V power at reduced costs provided by the MBAT RTP will be made possible through a new and very promising V&V approach in which model-based testing technologies will be combined with static analysis techniques. Besides this combination, a further new approach is to use (and re-use) specially designed analysis & test models (A&T models) as basis for model-based V&V. This advanced model-based V&V technology shall lead to a more effective and at the same time cost-reducing approach compared to those used so far.
Some key questions that are driving the project are the following:
- What kind of benefits would we get in case we would tightly combine/integrate static analysis & (model-based) testing (A&T) for an overall validation& verification approach?
- Can we save V&V costs and/or find more errors with this combination (compared to the actual V&V situation)?
- How could analysis results been used to steer testing and vice versa, how could testing results been used to steer analysis?
- Which (embedded) system parts or features should be analyzed and which should be tested?
- How does an overall A&T workflow look like that describes the analysis & testing combination?
- How does a underlying A&T model look like that supports this combination?
- How do tool chains & demonstrators look like which are supporting the combination of static analysis & testing?
- How can we show that the new approach is better than those approaches that we already have in our institutes & companies?
The talk will describe technical outcomes and experiences gained with MBAT and in addition present answers to the questions above.