«IST-004527 ARTIST2 NoE Year 4 Cluster: Testing and Verification D2-Mgt-Y4-VII IST-004527 ARTIST2 Network of Excellence on Embedded Systems Design ...»
IST-004527 ARTIST2 NoE Year 4
Cluster: Testing and Verification D2-Mgt-Y4-VII
Network of Excellence
on Embedded Systems Design
Cluster Progress Report for Year 4
Testing and Verification
Director, Professor Kim Guldstrand Larsen
CISS, Aalborg University, Denmark
Policy Objective (abstract)
The objective is to combine the efforts and skills of the individual leading researchers and research groups in Europe into a world-class virtual team, for advancing the state-of-the-art in verification and testing methodologies. Meeting place Testing and verification is a transversal topic interacting with all the other topics in embedded systems design aiming to ensure that the different design steps meet given properties as well as the overall correctness of the implementation. Focus within the cluster is on two aspects being of extreme importance for embedded systems. First is the verification and testing of quantitative properties ensuring that real-time constraints and quality of service constraints are met. Second is the verification of security properties. A particular objective is the successful transfer of knowledge, methods and tools to industry.
1/20 IST-004527 ARTIST2 NoE Year 4 Cluster: Testing and Verification D2-Mgt-Y4-VII Table of Contents
1.1 High-Level Objectives
1.2 Industrial Sectors
1.3 Main Research Trends
2. State of the Integration in Europe
2.1 Brief State of the Art
2.2 Main Aims for Integration and Building Excellence through Artist2
2.3 Other Research Teams
2.4 Interaction of the Cluster with Other Communities
3. Overall Assessment and Vision for the Cluster
3.1 Assessment for Year 4
3.2 Overall Assesment since the start of the Artist2 NoE
3.3 Vision Beyond the Artist2 NoE
4. Cluster Participants
4.1 Core Partners
4.2 Affiliated Industrial Partners
4.3 Affiliated International Partners
5. Internal Reviewers for this Deliverable
1. Overview In this section we give an overview of the current situation for the cluster’s research area in terms of overall objectives and trends.
1.1 High-Level Objectives The high level objectives for the 18 months period, February 2007 until August 2008, are as
• Quantitative Testing and Verification: included continued effort towards efficient tool components for controller synthesis, initiation of work on property-preserving code generation, development of generic frameworks using abstraction and compositionality for efficient analysis of quantitative models and new debugging and analysis techniques based on various combinations of testing and verification techniques. lskdjfjjsflksjfskjf Also, based on existing powerful (real-time) verification techniques work towards maturing and further development of important topics such as optimal scheduling, monitoring and fault diagnosis, controller synthesis, robustness and implementability of quantitative models and analysis of hybrid models, stochastic and timed models has been planned.
• Testing and Verification Platform for Embedded Systems: Systems the objectives include continued improvement related to the individual tools, their advancement and dissemination as well as application on industrial case studies. Also, the objectives include a high performance tools server.
• Verification of Security Properties: Based on a decision made at the last review, the activities on security have been embedded within the two activities above.
For Quantitative Testing and Verification almost all objectives have been accomplished.
Substantial research advancing state-of-the-art of controller synthesis has been made covering synthesis with budget constraints, partial observability, modular and distributed synthesis, costoptimality, synthesis with respect to bounded response properties.
A variety of quantitative models have been introduced and throurougly examined, including models with resources (e.g. cost, energy, memory consumption, stack size, etc) as well as stochastic aspects. Methods supporting compositionality and component based development using rich interfaces (i.e. quantitative component specifications) have been provided and abstraction of quantitative models (both stochastic and hybrid) have provided the basis for efficient analysis methods.
Novel debugging and analysis techniques have been provided including techniques based on heuristic and guided search, off-line test generation using games as well as symbolic model checking techniques.
Robustness and implementability has been subject to less activity than anticipated. However, within upcoming newly started FP7 STREP projects these topics will be pursued during the next years.
Within Testing and Verification Platform for Embedded Systems all objectives have been accomplished. The individual tools have been further refined – both with respect to functionality and performance. E.g. The tool UPPAAL TIGA now offers a mature tool for (timeIST-004527 ARTIST2 NoE Year 4 Cluster: Testing and Verification D2-Mgt-Y4-VII optimal) synthesis for timed games models with a growing number of industrial applications.
Also, the work of dissemination of the tools through case study demonstrators has been continued and documented through the joint web page for industrial case studies. Finally, the high performance tools server has been completed making the tools suitable for 64 bit architetures and distributed PC clusters available via a common web interface.
1.2 Industrial Sectors The testing and verification techniques and tools developed and disseminated within the cluster have relevance and potential impact on literally all industrial sectors developing or using embedded systems solutions. Within the Strategic Research Agenda of the ARTEMIS research platform1 Design Methods and Tools is one of the three research priorities put forward. Here model- and component-based approaches are proposed as necessary for coping with the growing complexity of systems while meeting “time-to-market” requirements.
Methods and tools for testing and verification are to play a central role in the ARTEMIS
research strategy, as can be seen from the following citations:
• “.. methods and tools for simulation, automatic validation and proving, and virtual Verification and Validation (V&V). Methods and tools for developing product lines of embedded systems.” • “.. reduce the cost of the system design by 50%. Matured product family technologies will enable a much higher degree of strategic reuse of all artifacts, while component technology will permit predictable assembly of Embedded Systems.” • “.. achieve 50% reduction in development cycles. Design excellence will aim to reach a goal of “right first time, every time” by 2016, including Validation, Verification and certification (to the same and higher standards as today).” • “..manage a complexity increase of 100% with 20% effort reduction. The capability to manage uncertainty in the design process and to maintain independent hardware and software upgradeability all along the life cycle will be crucial.” • “.. reduce by 50% the effort and time required for re-validation and recertification after change, so that they are linearly related to the changes in functionality.” The industrial needs for improved tools and methods for system validation have also been witnessed by a number of industrial and industry inspired case-studies and projects using model-based testing and verification carried out by the individual partners. Detailed information of these (and others) is to be found in the ARTIST2 Open Repository for Test and
Verification Case Studies (https://bugsy.grid.aau.dk/artist2), and include:
• Danfoss (Aalborg): The project has two main goals. One is to develop an automated test execution environment for system level testing of the EKC series refrigeration controllers. The other is to improve model-based online testing given the experiences from the first trials
• ESI (Embedded Systems Institute, Eindhoven) has carried out (is carrying out) large industrial case studies with Océ, ASML, Philips Semiconductors (now NXP), Philips Medical Systems, Vanderlande Industries.
• Ericsson Telebit (Aalborg): The goal of this project has been to use Live Sequence Charts in a model-driven approach to the testing of TCP/IP internet protocols. Live Sequence Charts are used to capture (informal) RFC in a formal, yet intuitive, way.
• Novo Nordisk A/S. (Aalborg) Automaic generation of test cases from UML statechart models of MMI (man machine interface) for medical devices. Each statechart model describe a specific class of usage scenarios, and test cases are derive in two steps.
First the model is translated into an equivalent timed automata. Then the automata is analysed based on various parameters (coverage criteria, search depth, etc) reslting in a number of test cases expressed in the company specific scripting language. The obtained coverage and possibly unreachable states are reported.
• OFFIS, University of Freiburg, Aalborg University: The "Single-tracked Line Segment" (SLS) case study stems from an industrial partner of the UniForM-project. It is the specification of a control system for a single-tracked line segment for tramways. It is implemented by distributed PLC automata. We took three different models of the SLS case study as examples. As the safety property to verify, we chose the mutual exclusion of drive permissions, i.e., the control system never gives permission to both directions simultaneously.
• OFFIS; Univ. of Oldenburg; Albert-Ludwigs-Universität Freiburg; Max-Planck-Institut für Informatik: The flap controller (high-lift) case study is derived from a case study for Airbus, a controller for the flaps of an aircraft. The flaps are extended during take-off and landing to generate more lift at low velocity. They are not robust enough for high velocity, so they must be retracted for other periods. The controller can perform a loadrelief function to correct the pilot's commands if he endangers the flaps. Additionally, there is also an extensive monitoring of the health of its sub-systems, checking for instance for hardware failures. Typically this will give rise to large discrete state spaces when model checking models derived from the flap controller.
• OFFIS, Univ. of Oldenburg : Automating verification of cooperation, control, and design in traffic applications. Here we present a verification methodology for cooperating traffic agents covering analysis of cooperation strategies, realization of strategies through control, and implementation of control. For each layer, we provide dedicated approaches to formal verification of safety and stability properties of the design. The range of employed verification techniques invoked to span this verification space includes application of pre-verified design patterns, automatic synthesis of Lyapunov functions, constraint generation for parameterized designs, model-checking in rich theories, and abstraction refinement. We illustrate this approach with a variant of the European Train Control System (ETCS), employing layer specific verification techniques to layer specific views of an ETCS design.
• Scott/Tiger Validate (Aalborg): From timed automata design models the verification engine of UPPAAL is used for off-line generation of test-sequences which covers the model. In the project a tool for translating these logical test-sequences to test-scripts executable in, e.g., QTP of Mercury’s Test Director. The resulting tool-chain has been applied to automatic testing of web-services of TDC (Danish Telecom). A commercial spin-off tool (V+) has been developed.
• Skov A/S (Aalborg): In this work, we provide a complete tool chain for automatic controller synthesis using UPPAAL Tiga and Simulink. The tool chain is explored using an industrial case study for climate control in a pig stable. The problem is modelled as a game, and UPPAAL Tiga is used to automatically synthesize a safe strategy that is transformed for input to Simulink, ´which is used to run simulations on the controller and generate code that can be executed in the actual pig stable. The models allow for guiding the synthesis process and generate different strategies that are compared through simulations.
• Dependable Systems and Software (DSS) group at Saarland university, Formal Methods and Tools group (FMT) and Design and Analysis of Communication Systems 5/20 IST-004527 ARTIST2 NoE Year 4 Cluster: Testing and Verification D2-Mgt-Y4-VII (DACS) group at the university of Twente: Arcade models. These include two case studies found in the literature, namely a Distributed Database Architecture and a Reactor Cooling System. Arcade tool was used which is based on the input/output interactive Markov chains formalism.
• DSS group at Saarland university, FMT and DACS groups at the university of Twente:
Dynamic Fault Tree (DFT) models These include four case studies that also appeared in the literature, namely the cascaded PAND system, the cardiac assist system, the multi-processor distributed computing system, and the fault-tolerant parallel processor.
Coral tool was used which is based on the input/output interactive Markov chains formalism.
• Software engineering group and FMT group at the university of Twente: Open-source Media Player. This case study was conducted on a publicly available open-source media player called MPlayer (http://www.mplayerhq.hu/). We have modeled the recovery mechanism implemented for the MPlayer and analyzed the availability of the system. Few tools were used including the FLORA framework and the CADP tool set (http://www.inrialpes.fr/vasy/cadp/). The input/output interactive Markov chains formalism was used.