Description
Cyber-physical systems (CPS) are integrations of heterogeneous collaborative entities that interact between themselves and with their physical environment. CPS exhibit complex and unpredictable behaviors, thus making their correctness and robustness analysis a challenging task. In order to address their full complexity, there is an emergent need for formal, yet efficient and scalable methods for the verification and analysis of CPS. Light-weight verification techniques, such as monitoring and testing, achieve both rigour and efficiency by enabling the evaluation of systems according to the properties of their individual behaviours. The MT CPS workshop aims at bringing together researchers and practitioners interested in the problems of detecting, testing, measuring and extracting qualitative and quantitative properties from CPS behaviors. Topics of interest include (but are not limited to):
- Specification languages for monitoring and testing
- Runtime verification and monitoring
- Black-box and white-box testing
- Measuring and statistical information gathering
- Simulation-based verification and parameter synthesis
- Diagnostics, error localization and repair
- Combination of static and dynamic analysis
- Applications and case studies
Workshop Format
MT CPS workshop is intended to be a forum for exchanging the latest scientific trends between researchers and practitioners interested in the field of light-weight verification and analysis of CPS. As a consequence, the workshop will NOT have formal proceedings. We encourage submission of abstracts that address any of the aforementioned topics of interest and cover recently published results as well as the work in progress.
Important Dates
- Abstract submission deadline:
February 14, 2016February 21, 2016 - Notification: March 5, 2016
- Early registration: March 18, 2016
- Workshop: April 11, 2016
Submission instructions
Abstracts are submitted via https://easychair.org/conferences/?conf=mtcps2016. Abstracts should be in PDF form, up to 2 pages in length with 1-inch margins and at least 10-point font size, and may contain up to two figures. Abstracts should list the full names, affiliations, and contact information of all authors, and the submission should indicate whether the abstract will be presented as a poster, orally, or both. Abstracts will be reviewed by the Program Committee. Those that are selected for oral and poster presentations will be distributed to workshop participants and posted on the workshop website.
Program Chairs
- Radu Grosu, Vienna University of Technology, Austria
- Oded Maler, VERIMAG, France
- Dejan Nickovic, AIT Austrian Institute of Technology GmbH, Austria
Program Committee
- Xavier Avon, EASii-IC, France
- Ezio Bartocci, Vienna University of Technology, Austria
- Sergiy Bogomolov, IST Austria, Austria
- Harald Brandl, AVL List GmbH, Austria
- Thao Dang, VERIMAG, France
- Jyotirmoy Deshmukh, Toyota Technical Center, USA
- Alexandre Donzé, UC Berkeley, USA
- Georgios Fainekos, Arizona State University, USA
- Thomas Ferrère, Mentor Graphics, France
- Christoph Grimm, Kaiserslautern University of Technology, Germany
- Radu Grosu, Vienna University of Technology, Austria
- Ichiro Hasuo, University of Tokyo, Japan
- Thomas Klotz, Bosch Sensortec GmbH, Germany
- Scott Little, Intel, USA
- Oded Maler, VERIMAG, France
- Thang Nguyen, Infineon Technologies AG, Austria
- Dejan Nickovic, AIT Austrian Institute of Technology GmbH, Austria
- Sriram Sankaranarayanan, University of Colorado at Boulder, USA
Keynote
Bernhard K. Aichernig
Associate Professor at Graz University of Technology, Austria
Bernhard K. Aichernig is a tenured associate professor, key researcher and project manager at Graz University of Technology, Austria. He is an expert in formal methods and model-based testing. His research focuses on the foundations of software engineering in order to achieve dependable computer-based systems. Since 2006, he runs European projects on this topic. Bernhard is also a board member of Formal Methods Europe (FME), an international organisation that promotes well-founded techniques in software engineering and organises the Formal Methods (FM) conferences.
From 2002 to 2006 he worked as a Research Fellow at UNU-IIST in Macao S.A.R., China, a research institute of the United Nations on software technology.
He holds a habilitation in Practical Computer Science and Formal Methods, a doctorate, and a diploma engineer degree from Graz University of Technology.
Killing Bugs in a Black Box with Model-based Mutation Testing
In this talk I will discuss the combination of model-based testing and mutation testing. Its central idea is to inject bugs in a model and generate a high-quality test suite that will kill these bugs in a system under test. We will cover its foundations, algorithms, tools and recent industrial applications. Model-based testing is a black-box testing technique that avoids the labour of manually writing hundreds of test cases, but instead advocates the capturing of the expected behaviour in a model of the system under test. The test cases are automatically generated from this model. The technique is receiving growing interest in the cyber-physical systems domain, where models are the rule rather than the exception. Mutation testing is a technique for assessing and improving a test suite. A number of faulty versions of a program under test are produced by injecting bugs into its source code. These faulty programs are called mutants. A tester analyses if the test suite can "kill" all mutants. We say that a test kills a mutant if it is able to distinguish it from the original. The tester improves the test suite until all faulty mutants get killed.
Venue
The Hofburg is the center of Vienna and the heart of the old city. On its opposite side, and separated by the beautiful People’s garden, is the magnificent, gothic-style city hall. Around the Hofburg Vienna offers one of the largest varieties of hotels and pensions in the world: From classic to modern, low to high budget, and pedestrian-zone-shopping-area to quiet-and-romantic-street view.
Additional information
How to register?
MT CPS 2016 is part of CPS Week 2016. In order to register for the workshop, please use the CPS Week 2016 central registration website.
Monday, April 11, 2016
Time | Talk | Slides |
---|---|---|
08h20-08h30 | Welcome | |
08h30-09h30 | Invited talk - Bernhard Aichernig. Killing Bugs in a Black Box with Model-based Mutation Testing | |
09h30-10h00 | Anna Lukina, Radu Grosu, Ezio Bartocci and Scott A. Smolka. Statistical Model Checking as Feedback Control | |
10h00-10h30 | Bardh Hoxha and Georgios Fainekos. Pareto Front Exploration for Parametric Temporal Logic Specifications of Cyber-Physical Systems | |
10h30-11h00 | Coffee break | |
11h00-11h30 | Thao Dang, Alie El-Din Mady, Boubekeur Menouer, Rajesh Kumar and Mark Moulin. Validation of Industrial Cyber-Physical Systems: an application to HVAC systems | |
11h30-12h00 | Thang Nguyen, Dirk Hammerschmidt, Andrei Basa and Gerald Klatzer. Sensor Network Emulyzer for advanced Automotive System Testing and Development | |
12h00-12h30 | Konstantin Selyunin and Stefan Jaksic. Many facets of Hardware Monitoring | ppt |
12h30-14h00 | Lunch | |
14h00-14h30 | László Balogh, István Dávid, István Ráth, Dániel Varró and András Vörös. Distributed and Heterogeneous Event-based Monitoring in Smart Cyber-Physical Systems | |
14h30-15h00 | Armin Wasicek. Cyber-Physical Intrusion Detection using Reference Models | |
15h00-15h30 | Tetsuya Tohdo. A Study of System and Software Testing based on Formal Verification Criteria | |
15h30-16h00 | Coffee break | |
16h00-16h30 | Adel Dokhanchi, Bardh Hoxha and Georgios Fainekos. MITL Specification Debugging for Monitoring of Cyber-Physical Systems | |
16h30-17h00 | Thomas Ferrère, Oded Maler and Dejan Nickovic. Trace Diagnostics for MTL Specifications | |
17h00-17h30 | Dogan Ulus. Montre: A Tool for Monitoring Timed Regular Expressions |