Formal Methods and Verification at ULB Computer Science Department at ULB

Almost ASAP semantics

The almost ASAP semantics is an alternative semantics for timed automata. This semantics is useful when modeling real-time controllers : control strategies modeled with this semantics are robust and implementable (without making the synchrony hypothesis).


Papers


  • Martin De Wulf, Laurent Doyen, Jean-François Raskin. Almost ASAP Semantics: From Timed Models to Timed Implementations. In HSCC 04, Hybrid Systems - Computation and Control, Lecture Notes in Computer Science 2993, pages 296-310, Springer Verlag, 2004. [Short version], [Long version with full proofs]
  • Martin De Wulf, Laurent Doyen, Nicolas Markey, and Jean-François Raskin. Robustness and Implementability of Timed Automata. In FORMATS/FTRTFT 04, Lecture Notes in Computer Science 3253, pages 118-133, Springer Verlag, 2004. [Short version]
  • Martin De Wulf, Laurent Doyen, Jean-François Raskin. Systematic Implementation of Real-Time Models. Accepted for publications in FM 2005, LNCS.[Short version]

Case Study


We verified and implemented automatically the audio control protocol introduced in [1]. It is a binary communication protocol using manchester encoding.We used the models of [2], which are provided with the HyTech tool, as a starting point. In our case study, we use the BrickOS operating system running on LEGO MINDSTORMS Bricks to implement the sender and the receiver. To connect the two Bricks, we use a wire plugged to an output gate of the sender and to an input gate of the receiver. For further informations refer to our latest paper.


For this case study, all the models for HyTech and Uppaal and the generated C code for BrickOs are available either as a compressed archive [audio.tgz] or one file at the time:

Verification files(*)
audioPerfect.hy A "perfect" HyTech modelization of the audio control protocol
audio.el The Elastic specification of the whole system
audio.hy The HyTech specification mutually similar to the AASAP semantics of the two controllers
audioGOOD.xml Uppaal model mutually similar to the hytech previous one with delta1=delta2=1/5 (satisfies the properties)
audioBAD.xml Uppaal model mutually similar to the hytech previous one with delta1=delta2=1/4 (does not satisfy the properties)
audio.q The reachability property for Uppaal
C code for BrickOS(*)
sender.c The code for the sender
receiver.c The code for the receiver

(*) Beware that to execute the code, you should download the gzipped archive that contains some necessary additional files. The files constitute a test program which will test sequentially different time scale for the protocol. It first uses a time unit of 80ms to send 1500 binary messages. If no error occurs, it will then send those 1500 messages again, decreasing the time unit by 10 ms and so on, and so forth until an error occurs.

[1] D. Bosscher, I. Polak, and F. Vaandrager. Verification of an Audio Control Protocol. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 863, pages 170-192, Lübeck, Germany, 1994. Springer-Verlag.
[.html ]
[2] P. H. Ho and H. Wong-Toi. Automated analysis of an audio control protocol. In P. Wolper, editor, Proceedings of the 7th International Conference On Computer Aided Verification, volume 939, pages 381-394, Liege, Belgium, 1995. Springer Verlag.
[.html ]
Tools


A first beta version of the verification part of our tool is available here. It generates models for verification using HyTech and Uppaal (3.4.8). The user manual will be available soon.

Involved Peoples




Last modification : May 2005