FINAL PROJECT REPORT
FINAL PROJECT REPORTAugust 2007Project no.: IST-2001-35304Project Co-ordinator: Frits VaandragerProject Start Date: 1 April 02Duration: 39 monthsProject home page: http://ametist.cs.utwente.nl/Status: Public
Contents1 Project Overview41.1Consortium Description . . . . . . . . . . . . . . . . . . . . . . . . . . . .41.2Main Achievements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .52 Project Objectives63 Project Methodologies, Results and Achievements73.1Model-Based System Development . . . . . . . . . . . . . . . . . . . . . .83.2Project Results: Expressiveness, Performance & Tools . . . . . . . . . . . .103.2.1Priced Timed Automata: Theory, Algorithms and Applications . .103.2.2Stochastic Extensions of Timed Automata . . . . . . . . . . . . . .113.2.3Modelling Frameworks for Scheduling Under (Discrete) Uncertainty113.2.4Optimization and Constraint Satisfaction as a Tool for Timed Automata Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . .123.2.5Improvements in Timed Automata Model Checking Technology . .123.2.6Specialized Technology for Solving Scheduling Problems with TimedAutomata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12Tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .13Project Results: Cybernetix Case Study . . . . . . . . . . . . . . . . . . .153.3.1Activities in year one and two . . . . . . . . . . . . . . . . . . . . .163.3.2Work in the third year . . . . . . . . . . . . . . . . . . . . . . . . .173.3.3Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .18Project Results: Terma Case Study . . . . . . . . . . . . . . . . . . . . . .193.4.1Summary of the work . . . . . . . . . . . . . . . . . . . . . . . . . .193.4.2Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .203.2.73.33.43.53.63.7Project Results: Bosch Case Studies. . . . . . . . . . . . . . . . . . . . .203.5.1The CPS Case Study . . . . . . . . . . . . . . . . . . . . . . . . . .203.5.2The Airbag ECU Case Study . . . . . . . . . . . . . . . . . . . . .22Project Results: Axxom Case Study . . . . . . . . . . . . . . . . . . . . . .253.6.1Problem Statement . . . . . . . . . . . . . . . . . . . . . . . . . . .263.6.2Modeling and Requirement Specification . . . . . . . . . . . . . . .273.6.3Tool Application and Solution . . . . . . . . . . . . . . . . . . . . .293.6.4Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .42Project Results: Other Case Studies2. . . . . . . . . . . . . . . . . . . . .44
3.8Towards a Unifying Framework . . . . . . . . . . . . . . . . . . . . . . . .454 Outlook475 Conclusions49A List of Deliverables733
1Project Overview1.1Consortium DescriptionThe Ametist consortium 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 oud University NijmegenBoschCybernetixAxxomTermaUniversity of AalborgUniversity of DortmundVERIMAGWeizmann InstituteLIF MarseilleUniversity of TwenteContact personFrits VaandragerMarko AuerswaldPatrice GauthierDagmar LudewigThomas HuneKim LarsenSebastian EngellOded MalerAmir PnueliPeter NiebertEd iderAlready before the start of Ametist , the academic partners have been cooperating successfully for many years in European projects. All academic partners share a commonmission, which is to conduct research on the application of formal methods for the development of computer based systems with the long range objective of transforming theapplication of formal methods from an academic research topic into an engineering practice. 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 schedulingVerimagtool builder (IF), timed systemsWeizmann synthesis, abstraction and composition techniquesMarseillesymbolic 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. Eachindustrial partner had a privileged relation with one of the academic partners: Bosch andAxxom with Dortmund, Cybernetix with Marseille, and Terma with Aalborg.4
1.2Main 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 spacecrafts.Typically, in each of these domain problems are solved using different approaches andmathematical tools. The Ametist project has provided the foundations for a unifyingframework for time-dependent behavior and dynamic resource allocation that crosses theboundaries of application domains.In the Ametist approach, components of a system are modeled as dynamical systems witha state space and a well-defined dynamics. All that can happen in a system is expressed interms of behaviors that 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 checking. Ametist has shown that this approach, which underlies thesuccessful domain of formal verification, can be extended to resource allocation, schedulingand other time-related problems.Ametist has made major advances in the area of (timed automata based) tools. Several(new versions) of tools were released, implementing algorithmic ideas that have been developed 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 of Ametist, 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 accessible.Profiting from the new tools, the Ametist consortium has tackled more than 20 industrialsized case studies which were provided by our industrial partners (Bosch, CYR, Axxom,Terma) or obtained from other sources. 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. Using Uppaal CORA, for instance, we succeeded to deriveschedules that are competitive with those that were provided by industrial partner Axxom1This subsection has been taken from [56].5
using 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 scheduling.2Project ObjectivesThe following description of the objectives of Ametist has been taken from the TechnicalAnnex.Ametist intends to contribute to solutions for the growing industrial need to design reliable and efficient time dependent systems. 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 systems.In addition to its technological contributions, Ametist invests actively in knowledge transfer to the European industry of computer-aided timing analysis and design. Moreover, itis expected that the academic dissemination of the Ametist research results will influence and advance the field of timed systems research, and (indirectly) contribute to theeducation of future generations of system engineers.Whereas 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. The aim of Ametist is to advanceand mature the related models, tools, and methods to allow this situation to change.The need for automatic tools that allow reasoning about time is evident. Beyond manufacturing, 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 industrialsetting.6
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 engineers.Ametist aims at the (at least partial) elimination of these obstacles. 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 systems, in particular in the area of real-time controller synthesis, planning and scheduling.Moreover, 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 field.3Project Methodologies, Results and AchievementsThe purpose of this section2 is to summarize the developments that took place within theAmetist project and put them in a larger scientific and technological context. We startwith a general overview of model-based design and analysis of systems from which theapproach advocated by Ametist has emerged. The principles underlying this approachare those underlying the verification of reactive computer systems. We then move to themore specific goal of the project, namely the exportation and adaptation of this approachto a wide class of systems where quantitative timing information plays a major role. Ithappens sometime that such systems are treated by techniques that do not follow theseprinciples for one or more of the following reasons:1. The communities in question follow their old ways and gave not assimilated thecomputer science way of looking at such problems;2. Being “semantically correct” is not the most urgent issue in these problem comparedto being able to express many real-life details and treat hard computational problems.It is sometimes believed that taking the trouble to formalize cleanly one does notprogress toward a solution and often adds another level of artificial complexity.Finally we mention some of the major achievements of the project and assess their contribution toward fulfilling that vision, or perhaps adapting it to real life in a more realisticmanner.2The material in this section is based on [53, 52, 48, 45, 46].7
3.1Model-Based System DevelopmentA large part of engineering and applied mathematics is concerned with building mathematical models of systems and using these models to validate the correct functioning of thesystem and to choose between design alternatives in order
1 Project Overview 1.1 Consortium Description The Ametist consortium is composed of seven academic partners and four industrial partners as indicated in the table below.
Final Exam Answers just a click away ECO 372 Final Exam ECO 561 Final Exam FIN 571 Final Exam FIN 571 Connect Problems FIN 575 Final Exam LAW 421 Final Exam ACC 291 Final Exam . LDR 531 Final Exam MKT 571 Final Exam QNT 561 Final Exam OPS 571
Project Acronym: Kultur Version: Final Contact: whw@soton.ac.uk Date: 30.03.09 Page 1 of 29 Document title: JISC Final Report Last updated: March 2008 JISC Final Report Project Document Cover Sheet Project Information Project Acronym Project Title Kultur Start Date March 2007 End Date March 2009 Lead Institution University of Southampton Project
ART 224 01 05/01 04:00 PM AAH 208 ART 231 01 05/02 04:00 PM AAH 138 . Spring 2019 Final Exam Schedule . BIOL 460 01 No Final BIOL 460 02 No Final BIOL 460 03 No Final BIOL 491 01 No Final BIOL 491 02 No Final BIOL 491 03 No Final BIOL 491 04 No Final .
DIDET Project – Final Report – 1.0 – 1st August 2008 Page 1 of 26 JISC DEVELOPMENT PROGRAMMES Project Document Cover Sheet DIDET Project Final Report Project Project Acronym DIDET Project ID Project Title Digital Libraries for Distributed, Innovative Design Education and Teamwork Start Date 1 March 2003 End Date 29 February 2008
ME 2110 - Final Contest Timeline and Final Report Preparation March 31, 2014 C.J. Adams Head TA . Agenda 2 Overview of this week Final Contest Timeline Design Review Overview Final Report Overview Final Presentation Overview Q&A . MARCH Monday Tuesday Wednesday Thursday Friday .
ANTH 330 01 No Final Spring 2020 Final Exam Schedule . ART 221 01 No Final ART 223 01 No Final ART 224 01 05/11 04:00 PM AAH 208 . BIOL 693 01 No Final BIOL 696 01 No Final BLBC 518 01 05/12 04:00 PM CL 213 BLBC 553 01 No Final CEP 215 01 05/12 06:00 PM G303 CEP 215 02 05/11 10:30 AM WH106B .
FoNS guidelines for writing a final project report July 2012 1 Guidelines for writing a final project report July 2012 FoNS has a strong commitment to disseminating the work of the project teams that we support. Developing and changing practice to improve patient care is complex and we therefore believe it is essential to share the outcomes, learning and experiences of those involved in such .
Jul 04, 2020 · Final Project Report – April 2007 . Virgin River Conservation Partnership 2005-OLVF-611-P-2005-01 . . Did the project encounter internal or external challenges? No . How were they addressed? N/A . . Final Project Report Format .
