VHS Workpackage TL.1: Tools

This document exists also as PS file.

Overview of Tool Developments

In addition to improvements of existing tools for timing analysis, such as Uppaal and Kronos, some new prototype tools have been developed and tested. Among them one can find Moreover, significant contributions to the existing commercial tool visualSTATE (a UML-based tool for design, validation and verification, prototyping and code-generation of embedded control software) have been made: Jointly, these efforts contributes to the enhancement of the computer support for plant analysis and has helped in solving the verification problems encountered in the case-studies. The tool efforts are described below in more detail.

UPPAAL

Uppaal (see also http://www.uppaal.com) is a tool for modeling, simulation and verification of real-time systems modeled as networks of timed automata extended with data variables. The tool has been developed jointly by BRICS at Aalborg University and the Department of Computer Systems at Uppsala University since 1995. Here we give a summary of the various improvements and extensions of Uppaal carried out in the context of VHS during the last two years period.
In July 1999 a new version of Uppaal, called Uppaal2k, was released [PL00]. The new version, which required almost two years of development, is designed to improve the graphical interface of the tool, to allow for easier maintenance, and to be portable to most common operating systems while preserving Uppaal's ease-of-use and efficiency. To meet these requirements the new version is designed as a client/server application with a verification server providing efficient C++ services to a Java client over a socket based protocol. This design also makes it possible to execute the server and the GUI on two different machines. Compared to its predecessors Uppaal2k has a somewhat richer modeling language. The new language supports process templates and more complex (bounded) data structures, such as data variables, constants, arrays etc. The new Uppaal2k verification server contains some recent development in the area (see more below) as well as well-known verification techniques described elsewhere in the literature including bit-state hashing, convex-hull over-approximation and inactive clock reduction. Uppaal2k is currently available for Linux, SunOS and MS Windows platforms. It can be downloaded from the Uppaal home page. Since its release more than 500 users in 35 countries have been downloading the tool.
A main focus of the Uppaal research is to constantly search for more efficient algorithms and data structures for the verification of timed systems. In a series of papers [LWYP99][BLP{ et. al. }99][LWYP99] a new data structure called Clock Difference Diagrams (CDDs) has been developed. CDDs is a BDD-like data-structure intended for efficient representation and efficiently manipulation of non-convex subsets of the Euclidean space encountered during the verification of timed automata. The CDD data-structure has been implemented in Uppaal as an alternative to the classical data-structure of DBMs. In an experiment based on eight industrial examples the CDD-data-structure has demonstrated to yield space savings between 46% and 99% with moderate increase in run time. Currently, a full TCTL model-checker based on CDDs is being implemented.
For untimed systems the technique of partial-order reduction has in several practical cases proved extremely useful in dealing with the phenomena of state-explosion. The technique exploits independence between components in order to settle model-checking problems by only examining part of the state space. In [BJLY98] a serious attempt of providing a partial-order reduction method for timed systems based on a local-time semantics for networks of timed automata is given. However, the implicit global synchronization on time-progress for timed systems has proved to be a major obstacle in obtaining reductions and research is therefore still going on before the method will be part of the distributed version of Uppaal.
In [BHV00] a distributed version of Uppaal has been implemented. Based on four real life examples it is demonstrated that the combined processing and memory resources of multiple computers can be effectively utilized. The approach is successfully applied to both a network of workstations and a symmetric multiprocessor machines. A main observation is that the search order of the symbolic state space is crucial for the effectiveness and scalability of the exploration. The distributed implementation will soon be available as part of the standard Uppaal2k distribution.
A major problem in model-checking timed systems is the huge memory requirements. In particular, when the memory requirements exceeds that of the main memory good memory managements strategies are extremely important. A new method for controlling the memory-block traversal strategies is developed and implemented in Uppaal [LPY00] and experimentally demonstrated to significantly improve the performance of the tool.
Extending timed automata with stopwatches turns out to yield (at least) the full expressive power of linear hybrid automata. Moreover, stopwatch automata allow for (over-approximating) reachability analysis based on the simple data-structures of DBMs or CDDs, thus avoiding the complications of representing and manipulating general polyhedra. This method for analyzing linear hybrid automata has been developed, implemented within Uppaal and investigated through preliminary experiments in [CL00].
An important part of the development of Uppaal is the constant application of the tool to real case studies. During the past two years a number of such have been carried out. In [HLS99] a power-down protocol for an IR communication link is developed, modeled and verified using Uppaal in close collaboration with Bang & Olufsen. Similarly, [DY00] reports on an ongoing development project with ABB on a field-bus protocol. In [Hun99] and [IKL{ et. al. }00] control programs for controlling LEGO MINDSTORM systems (written in the programming language Not Quite C, NQC.) are automatically translated into Uppaal models permitting analysis and verification to be performed. The translations faithfully reflects the scheduling policy applied in the underlying operating system.
Within the VHS project the tasks VHS Case Study 1 and VHS Case Study 5 have proved very useful case studies for the tool. For VHS Case Study 1 [KLPW99] reports on a method allowing Uppaal to be used in an exact modeling and verification of arbitrary hybrids under certain assumptions. For VHS Case Study 5 Uppaal is used to synthesize production schedules (and later control programs) for batch processes ([HLP99] and [HLP00]). A general methodology of adding guidance to a model is given allowing schedules for 60 batches to be produced. We refer to the task descriptions for VHS Case Study 1 and VHS Case Study 5 for more detailed information.
Finally, Uppaal has been used as the basic tool in courses on real-time systems both at The Technical University of Denmark (see http://www.it.dtu.dk/c49411/) and at Aalborg University (see http://www.cs.auc.dk./~jelling/datateknik.html).

Kronos

Kronos [BDM{ et. al. }98] is the tool developed at VERIMAG for verifying real-time systems modeled as networks of communicating timed automata. An overall description of Kronos is provided in [Yov00] and [JY00]. Here we summarize the improvements and extensions of Kronos carried out during the last two years in the context of the VHS project.
We have implemented two algorithms for synthesizing a controller that prevents the system to take transitions that violate the desired property. The first algorithm [AGP{ et. al. }99] takes as input a timed automaton A, where transitions are labeled as ``controllable'' or ``uncontrollable'', and a TCTL formula f of the form AG P (read ``always P'') and EF P (read ``eventually P''), and it computes the set Q of states of A that satisfy f regardless of the uncontrollability of some transitions. A is then constrained by Q to obtained a timed automaton AQ that characterizes all the sequences of controllable transitions that keep the system only in states where Q is satisfied for any uncontrollable behavior. The second algorithm [TA99] works on-the-fly, but it does not necessarily constructs the maximal controller.
Based on its past experience, the research team at VERIMAG invested a great effort in designing and implementing a new tool based on the modules for timing analysis developed in Kronos and the libraries for graph manipulation provided by Cadp, a tool box for verification of untimed systems also developed at VERIMAG. This new tool is called Open Kronos and is described in detail in [Yov00]. In Open Kronos clocks can be either continuous or discrete. When discrete-valued clocks are used, a BDD-based verification tool can be used. The unified GUI for Kronos and Open Kronos that has been developed is described in [JY00]. One specific capability of Open Kronos that has been implemented in the context of the VHS project is the algorithm for checking for reachability properties and finding Büchi-accepting cycles on-the-fly. This module also produces time-stamped traces for failure diagnosis [Tri99].
Open Kronos has been successfully used in [NY00] for synthesizing optimal operation schemes in multi-batch chemical plants (VHS Case Study 1). In this context we developed routines for interpreting the timed traces found by Open Kronos as Gantt-Diagrams, for visualisation of resource usage over time, and as conflict free safe Petri nets, which represent the resolved decisions on resource conflicts. While the latter serve as basis for actual control code of the case study plant, we have furthermore used them to generate adapted input for GraphViz for visualisation. Examples of both kinds of interpretations of timed sequences for scheduling applications can be found in [NY00]. For experiments with the BDD-based verification algorithm of Open Kronos, a visualisation of the time and memory consumption was developed. Outputs of this visualisation can be found in [NY00].

Analysis of Hybrid Systems and Programmable Logic Controllers

The d/dt system

d/dt is an experimental tool [ABDM00] developed at VERIMAG for verification and controller synthesis for hybrid systems defined by linear differential equations and inclusions. It is based on approximate computations of sets of reachable state using a combination of techniques coming from numerical analysis, computational geometry, optimal control and verification. The systems accepts as input a description of a hybrid automaton and a set of states and can compute the successors of this set, verify safety properties, synthesize controllers and more. It is fair to say that it is the most advanced tool so far to treat hybrid systems. The system is put on the public domain and there is an ongoing effort to distribute it among potential users in automotive control, robotics and process control and improve its performance based on the accumulated experience in these and other domains. DDT has been developed at VERIMAG by Thao Dang, Eugene Asarin and Oded Maler.

YAHMST

YAHMST (Yet Another Hybrid Modeling and Simulation Toll) allows for hierarchical descriptions of hybrid systems which may be compiled into models corresponding to different configuration of the real system. These model can then be used to simulate process evolution. YAHMST has been developed by Luc Thevenon and Jean-Marie Flaus, Grenoble.

VERDICT

VERDICT is a modeling environment intending to make formal verification applicable to logic controlled chemical plants. The tool offers textual as well as graphical editors to set up models of the plant and controller. The tool automatically translates these models into (over-approximating) models (e.g. timed automata) that are verifiable with existing model-checking tools. VERDICT has been developed by Kowalewski, Bauer, Preussig, Stursberg and Treseler, Dortmund.

Hybrid System Animator using CVODE and Uppaal

A real-time animator for hybrid systems based on a discrete semantics has been developed [ADY00]. The tool can be used to simulate the dynamical behavior of a hybrid system in a real-time manner. The animator implements the discrete semantics for a given automaton and sampling period, using the differential equation solver CVODE. Currently, the engine of the animator has been implemented in Java and C using CVODE. The aim is a graphical user interface for editing and showing moving graphical objects and plotting curves. The graphical objects act on the screen according to physical laws described as differential equations and synchronize with controllers described as timed automata in Uppaal. The tool has been developed by Tobias Amnell, Alexandre David and Wang Yi, Uppsala.

Static analysis of PLCs

A verification tool aiming to automatically detect run-time errors in Instruction List programs before program execution is under development . In order to make this tool accessible to non-computer scientists, who do the everyday programming of PLCs, the focus on a "push button" tool where the required user-interaction is minimal. Therefore, the properties to be checked are of generic nature, like division by zero, infinite loops, dead code, whether array boundaries are exceeded etc. The tool is based on static analysis techniques in particular abstract interpretation and and data flow analysis as presented in [BHLL00c]. Since these techniques allow to use algorithms which are mostly linear or at most polynomial in time very large IL programs can be checked.

Analysis of Probabilistic Systems

The PDG system is a prototype tool [BM99a] for representing large-scale discrete-time probabilistic systems using a novel data-structure tailored for this purpose. The input for PDG is a set of communicating probabilistic automata and the output is a representation of the long-term probability over the global state-space of the system, i.e. an eigenvector of the system. PDG has been developed by Marius Bozga and Oded Maler, Grenoble.

visualSTATE

visualSTATE is a UML-based, commercial tool for design, validation and verification, prototyping and code-generation of embedded software. In collaboration with the company a new, now patented verification technique --- so-called compositional backwards technique --- has been developed which dramatically improves verification runtimes by decoupling independent states and collapsing states that behave similarly. Very encouraging results have been obtained on exhaustive verification of a large number of industrial applications. In the new release, the tool is now able to handle systems with more than 1,400 concurrent components in a few minutes on a standard PC. The compositional backwards technique was first presented in [LNAB{ et. al. }98] and has recently been presented in IEEE Computer [SLA{ et. al. }00]. An extension of the technique to statechart-like models which do not suffer from increase in the hierarchical depth but rather exploits the hierarchy is also given [BLAHH99]. The work on visualSTATE was a collaboration between the company visualSTATE and the research teams at BRICS, Aalborg University, and Department of Computer Systems, Technical University of Denmark.

Attached documents of the deliverable TL.1

  1. [ABDM00] Reachability analysis of piecewise-linear dynamical systems.
    E. Asarin, O. Bournez, T. Dang, and O. Maler.In B. Krogh and N. Lynch, editors, Hybrid Systems: Computation and Control, volume 1386 of LNCS, pages 20--31. Springer, April 2000.
    Download
    .Bibtex entry: Asarin:et:al00:linear.
  2. [ADY00] A real time animator for hybrid systems.
    Tobias Amnell, Alexandre David, and Wang Yi.Accepted for in the proceedings of 6th ACM SIGPLAN LCTES'2000., 2000.
    Download
    .Bibtex entry: AmDaWa00.
  3. [AGP et al. 99] A framework for scheduler synthesis.
    K. Altisen, G. Goessler, A. Pnueli, J. Sifakis, S. Tripakis, and S. Yovine.In IEEE Computer Society, editor, RTSS 1999 proceedings, pages 154--163, 1999.
    Download
    .Bibtex entry: AltisenGoesslerPnueliSifakisTripakisYovine99.
  4. [BDM et al. 98] Kronos: A model-checking tool for real-time systems.
    M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine.In Proc. 1998 Computer-Aided Verification, CAV'98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998. Springer-Verlag.
    Download
    .Bibtex entry: Kronos98.
  5. [BHLL00c] Utilizing static analysis for programmable logic controllers.
    Sébastien Bornot, Ralf Huuck, Yassine Lakhnech, and Ben Lukoschus.In ADPM 2000: 4th International Conference on Automation of Mixed Processes: Hybrid Dynamic Systems, September 18-19, 2000, Dortmund, Germany, 2000.
    Download
    .Bibtex entry: BHLL00:static.
  6. [BHV00] Distributed timed model checking - How the search order matters.
    Gerd Behrmann, Thomas Hune, and Frits Vaandrager.In Proc. of 12th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Chicago, Juli 2000. Springer-Verlag.
    Download
    .Bibtex entry: BeHuVa00.
  7. [BJLY98] Partial Order Reductions for Timed Systems .
    J. Bengtsson, B. Jonsson, J. Lilius, and W. Yi.In Partial Order Reductions for Timed Systems, Nice, France. Springer Verlag, 1998.
    Download
    .Bibtex entry: bjlw98:partialorder.
  8. [BLAHH99] Verification of Hierarchical State/Event Systems using Reusability and Compositionality.
    G. Berhmann, K. G. Larsen, H. R. Andersen, and J. L.-Nielsen H. Hulgaard.In Proceedings of TACAS'}99, Amsterdam, The Netherlands. LNCS 1579. Springer Verlag, 1999.
    Download
    .Bibtex entry: blahn99:hierarchical.
  9. [BLP et al. 99] Efficient Timed Reachability Analysis Using Clock Difference Diagrams .
    G. Behrmann, K. Larsen, J. Pearson, C. Weise, and W. Yi.In Proceedings of CAV99, pages 22--24. Springer Verlag, 1999.
    Download
    .Bibtex entry: blpww99:cdd.
  10. [BM99a] On the representation of probabilities over structured domains.
    M. Bozga and O. Maler.In N. Halbwachs and D. Peled, editors, Proc. CAV'99, volume 1633 of LNCS, pages 261--273. Springer, June 1999.
    Download
    .Bibtex entry: BozgaMaler99:PDG.
  11. [CL00] The impressive power of stopwatches.
    Franck Cassez and Kim G. Larsen.To appear in Proceedings of CONCUR'2000, 2000.
    Download
    .Bibtex entry: CaLa00.
  12. [DY00] Debugging a commercial field bus protocol.
    Alexandre David and Wang Yi.To appear in the proceedings of the 12th Euromicro Conference On ReaL-Time Systems., 2000.
    Download
    .Bibtex entry: DaWa00.
  13. [HLP99] Guided Synthesis of Control Programs using UPPAAL for VHS Case Study 5.
    Thomas Hune, Kim G. Larsen, and Paul Pettersson.BRICS, University of AArhus and University of Aalborg, Denmark, June 1999.
    Download
    .Bibtex entry: hlp99:guided.
  14. [HLP00] Guided synthesis of control programs using Uppaal.
    Thomas Hune, Kim G. Larsen, and Paul Pettersson.In Ten H. Lai, editor, Proc. of the IEEE ICDCS International Workshop on Distributed Systems Verification and Validation, pages E15--E22. IEEE Computer Society Press, April 2000.
    Download
    .Bibtex entry: HuLaPe00.
  15. [HLS99] Formal verification of a power controller using the real-time model checker UPPAAL.
    K. Havelund, K. Larsen, and A. Skou.In 5th International AMAST Workshop on Real-Time and Probabilistic Systems, 1999.
    Download
    .Bibtex entry: hls99:power.
  16. [Hun99] Modelling a real-time language.
    Thomas Hune.In Proceedings of FMICS, 1999.
    Download
    .Bibtex entry: hune99:modelling.
  17. [IKL et al. 00] Model-checking real-time control programs --- Verifying LEGO mindstorms systems using Uppaal.
    Torsten K. Iversen, Kaare J. Kristoffersen, Kim G. Larsen, Morten Laursen, Rune G. Madsen, Steffen K. Mortensen, Paul Pettersson, and Chris B. Thomasen.To appear in ECRTS'2000., 2000.
    Download
    .Bibtex entry: IKLLMMPT00.
  18. [JY00] An integrated GUI for Kronos and Open Kronos.
    Hou Jiamin and Sergio Yovine.VHS Deliverable TL.1 - Tools, 2000.
    Download
    .Bibtex entry: app:kronos-gui.
  19. [KLPW99] VHS Case Study 1 - Experimental Batch Plant using UPPAAL.
    K. Kristoffersen, K. Larsen, P. Pettersson, and C. Weise.BRICS, University of Aalborg, Denmark, May 1999.
    Download
    .Bibtex entry: KLPW99:cs1.
  20. [LNAB et al. 98] Verification of Large State/Event Systems Using Compositionality and Dependency Analysis.
    Jorn Lind-Nielsen, Henrik Reif Andersen, Gerd Behrmann, Henrik Hulgaard, Kaare J. Kristoffersen, and Kim G. Larsen.In Bernard Steffen, editor, Proc. of the 4em th Conference on Tools and Algorithms for the Construction and Analysis of Systems, number 1384 in Lecture Notes in Computer Science, pages 201--216. Springer--Verlag, 1998.
    Download
    .Bibtex entry: labhkl:tacas98.
  21. [LPY00] On Memory-Block Traversal Problems in Model Checking Timed Systems.
    Fredrik Larsson, Paul Pettersson, and Wang Yi.In Susanne Graf and Michael Schwartzbach, editors, Proc. of the 6em th Conference on Tools and Algorithms for the Construction and Analysis of Systems, number 1785 in Lecture Notes in Computer Science, pages 127--141. Springer--Verlag, 2000.
    Download
    .Bibtex entry: lpw:tacas00.
  22. [LWYP99] Clock difference diagrams.
    K. G. Larsen, C. Weise, W. Yi, and J. Pearson.Technical Report 98/99, ISSN 0283-0574, DoCS, Uppsala University, august 1999.
    Download
    .Bibtex entry: lwyp98:cdd.
  23. [LWYP99] Clock difference diagrams.
    Kim G. Larsen, Carsten Weise, Wang Yi, and Justin Pearson. Nordic Journal of Computing, 6(3):271--298, 1999.
    Download
    .Bibtex entry: LWWP99.
  24. [NY00] Computing optimal operation schemes for chemical plants in multi-batch mode.
    P. Niebert and S. Yovine.In Proc. Hybrid Systems, Computation and Control, HSCC'00, LNCS, Pittsburgh, PA, USA, March 2000. Springer-Verlag.
    Download
    .Bibtex entry: NiebertYovine00a.
  25. [NY00] Synthesis and dispatching of production schemes of chemical batch plants.
    Peter Niebert and Sergio Yovine.In to appear in proceedings of ADPM'00, 2000.
    Download
    .Bibtex entry: NiYo00b.
  26. [PL00] Uppaal2k.
    Paul Pettersson and Kim G. Larsen. Bulletin of the European Association for Theoretical Computer Science, 70:40--44, February 2000.
    Download
    .Bibtex entry: PeLa00.
  27. [SLA et al. 00] Practical verification of embedded software.
    Jorgen Staunstrup, Kim G. Larsen, Henrik Reif Andersen, Henrik Hulgaard, Gerd Behrmann, Kaare J. Kristoffersen, Jorn Lind-Nielsen, and Henrik Leerberg. IEEE Computer, May 2000.
    Download
    .Bibtex entry: SLAHBKLL00.
  28. [TA99] On-the-fly controller synthesis for discrete and dense time systems.
    S. Tripakis and K. Altisen.In Formal Methods 1999 (FM'99), volume I of LNCS 1706, pages 233--252, Toulouse, France, September 1999. Springer.
    Download
    .Bibtex entry: tripakis:altisen:1999:fm99.
  29. [Tri99] Timed diagnostics for reachability properties.
    S. Tripakis.In Tools and Algorithms for the Construction and Analysis of Systems, TACAS'99, Amsterdam, Holland, 1999.
    Download
    .Bibtex entry: Tripakis99.
  30. [Yov00] A brief summary of the tool Kronos.
    Sergion Yovine.VHS Deliverable TL.1 - Tools, 2000.
    Download
    .Bibtex entry: app:kronos.

page created at Tue May 30 17:09:13 MET DST 2000 by Peter Niebert
last modification: Thu Jun 29 15:32:07 CEST 2000