FINAL PROJECT REPORT - Radboud Universiteit

1 FINAL PROJECT REPORTA ugust 2007 PROJECT no.: IST-2001-35304 PROJECT Co-ordinator: Frits VaandragerProject Start Date: 1 April 02 Duration: 39 monthsProject home page: : PublicContents1 PROJECT Consortium Description .. Main Achievements .. 52 PROJECT Objectives63 PROJECT Methodologies, Results and Model-Based System Development .. PROJECT Results: Expressiveness, Performance & Tools .. Priced Timed Automata: Theory, Algorithms and Applications .. Stochastic Extensions of Timed Automata .. Modelling Frameworks for Scheduling Under (Discrete) Uncertainty Optimization and Constraint Satisfaction as a Tool for Timed Au-tomata Analysis .. Improvements in Timed Automata Model Checking Technology .. Specialized Technology for Solving Scheduling Problems with TimedAutomata.

2 Tools .. PROJECT Results: Cybernetix Case Study .. Activities in year one and two .. Work in the third year .. Conclusions .. PROJECT Results: Terma Case Study .. Summary of the work .. Conclusions .. PROJECT Results: Bosch Case Studies .. The CPS Case Study .. The Airbag ECU Case Study .. PROJECT Results: Axxom Case Study .. Problem Statement .. Modeling and Requirement Specification .. Tool Application and Solution .. Conclusions .. PROJECT Results: Other Case Studies .. Towards a Unifying Framework .. 454 Outlook475 Conclusions49A List of Deliverables7331 PROJECT Consortium DescriptionTheAmetistconsortium is composed of seven academic partners and four industrialpartners as indicated in the table below. The coordinator is listed first, followed by theindustrial partners on places 2-5, followed by the other academic partners on places personRoleCO1 Radboud University NijmegenFrits VaandragerTechnology ProviderAC2 BoschMarko AuerswaldUserAC3 CybernetixPatrice GauthierUserAC4 AxxomDagmar LudewigUserAC5 TermaThomas HuneUserCR6 University of AalborgKim LarsenTechnology ProviderCR7 University of DortmundSebastian EngellTechnology ProviderCR8 VERIMAGOded MalerTechnology ProviderAC9 Weizmann InstituteAmir PnueliTechnology ProviderCR10 LIF MarseillePeter NiebertTechnology ProviderCR11 University of TwenteEd BrinksmaTechnology ProviderAlready before the start ofAmetist, the academic partners have been cooperating suc-cessfully for many years in European projects.

3 All academic partners share a commonmission, which is to conduct research on the application of formal methods for the de-velopment of computer based systems with the long range objective of transforming theapplication of formal methods from an academic research topic into an engineering prac-tice. Even though the academic partners have a common background knowledge whichfacilitates collaborative work, they all brought in complementary expertise:Nijmegen verification and analysis of distributed real-time algorithms andsystems, model checking, application of formal methodsAalborgtool builder (Uppaal), model checkingDortmund process control, hybrid systems, production planning and schedul-ingVerimag tool builder (IF), timed systemsWeizmann synthesis, abstraction and composition techniquesMarseille symbolic verification, constraint programmingTwentevalidation tools, stochastic methods, verification of soft real-timesystemsThe industrial partners, which are all prominent players in the embedded systems area,contributed complementary case studies, and used and evaluated the PROJECT results.

4 Eachindustrial partner had a privileged relation with one of the academic partners: Bosch andAxxom with Dortmund, Cybernetix with Marseille, and Terma with Main AchievementsScheduling and resource allocation problems occur in many different domains1, for instance(1) scheduling of production lines in factories to optimize costs and delays, (2) schedulingof computer programs in (real-time) operating systems to meet deadline constraints, (3)scheduling of micro instructions inside a processor with a bounded number of registers andprocessing units, (4) scheduling of trains (or airplanes) over limited quantities of railwaytracks and crossroads, and (5) mission planning for autonomous robots on , in each of these domain problems are solved using different approaches andmathematical tools. TheAmetistproject has provided the foundations for a unifyingframework for time-dependent behavior and dynamic resource allocation that crosses theboundaries of application theAmetistapproach, components of a system are modeled asdynamical systemswitha state space and a well-defined dynamics.

5 All that can happen in a system is expressed interms ofbehaviorsthat can be generated by the dynamical systems; these constitute thesemantics of the problem. Verification, optimization, synthesis and other design activitiesexplore and modify system structure so that the resulting behaviors are correct, optimal,etc. Preferably, the limitations of currently known computational solutions should notinfluence modeling too much: only after the semantics of a problem is properly understood,abstractions and specialization due to computational considerations can intervene. In suchsituations, the soundness of abstractions should ideally also be proved, either via deductiveverification or model shown that this approach, which underlies thesuccessful domain offormal verification, can be extended to resource allocation, schedulingand other time-related made major advances in the area of (timed automata based) tools.

6 Several(new versions) of tools were released, implementing algorithmic ideas that have been devel-oped during the first two years of the PROJECT . Tight connections and interfaces between allof these tools exist or are currently being developed. If we compare the current capabilitiesof our tools with what existed at the start ofAmetist, then it is fair to say that indeed wehave moved the state-of-the-art to a new level of maturity (one of the main objectives ofthe PROJECT ). Also the convenience of using the tool has been greatly improved due to theenriched expressiveness of the input language and connections with other tools. Nowadayseven high school students find it easy to modify and build timed automata models usingthe improved GUI. Through the website and new tutorial papers (such as [94]) the toolhas become very easily from the new tools, theAmetistconsortium has tackled more than 20 industrialsized case studies which were provided by our industrial partners (Bosch,CYR,Axxom,Terma) or obtained from other sources.

7 The general conclusion is that using our newmethods we can handle bigger problems faster and in a much more routine manner thanat the start of the PROJECT . UsingUppaalCORA, for instance, we succeeded to deriveschedules that are competitive with those that were provided by industrial partnerAxxom1 This subsection has been taken from [56].5using its own tool Orion-Pi. Our experience with the AXXOM case study shows theapplication of model checking techniques for scheduling is promising. Still, timed automataare not yet a push-button technology to be applied without problem specific modeling andsolution strategies. But the generation of libraries of templates for typical configurationsseems promising and appears as a path towards to more widespread and easier applicationfor non-TA-specialist users. Considerable further work on modelling methods, reusebility ofmodelling patterns, identification and evaluation of heuristics, compasison with alternativeapproaches, all in the context of case studies of greater orders of magnitude, is needed todevelop it into a readily applicable standard technique for PROJECT ObjectivesThe following description of the objectives ofAmetisthas been taken from the to contribute to solutions for the growing industrial need to design re-liable and efficient time dependent systems.

8 In particular, it intends to provide theoryand tools for error-detection, control and optimisation of real-time distributed systems. Itsapproach will be based on translating state-of-the-art academic research into methods andtools that can be a basis for an industrial design practice of such addition to its technological contributions,Ametistinvests actively in knowledge trans-fer to the European industry of computer-aided timing analysis and design. Moreover, itis expected that the academic dissemination of theAmetistresearch results will influ-ence and advance the field of timed systems research, and (indirectly) contribute to theeducation of future generations of system timed automata and the tools for their analysis are widely accepted in academiaand are being used at hundreds of universities and research laboratories all around theworld, they have yet to find their way into industry.

9 The aim ofAmetistis to advanceand mature the related models, tools, and methods to allow this situation to need for automatic tools that allow reasoning about time is evident. Beyond manu-facturing, telecommunication and hardware, it is of essential importance for the growingmarket of embedded systems (from car electronics to home automation). However, thereare several obstacles that seem to hinder the use of timed automata technology in industryat this time: Scalability: Currently, tools based on timed automata do not allow to handle bigexamples. There are industrial scale examples that have been treated with thesetools but only after tedious manual simplification involving a lot of work in eachcase. Convenience: Current timed automata tools are stand-alone programs and theirinput formalisms lack important features for convenient specification in an Accessibility: To make optimal use of the currently available tools requires quitesome sophistication on the user s part, which makes them practically inaccessibleeven to well-trained at the (at least partial) elimination of these obstacles.

10 The PROJECT movestowards this goal along several tracks. One is the treatment of real-life case studies fromsome candidate application domains to see if, indeed, the proposed models, tools andmethodology are suited for them. Indeed much of the PROJECT s resources are being spenton case studies. A second direction aims to improve the situation regarding scalability,by introducing better algorithms and data-structures to model and manipulate large sys-tems, in particular in the area of real-time controller synthesis, planning and , the PROJECT aims at tool interaction to allow the interfacing of different tools,which can help to improve usability/convenience. The third track aims at synthesizing theaccumulated results in order to assess the applicability of the PROJECT s vision and modifyit according to feedback from the PROJECT Methodologies, Results and AchievementsThe purpose of this section2is to summarize the developments that took place within theAmetistproject and put them in a larger scientific and technological context.