Abstract : In this paper, we address the case study proposed by Habrias- namely specifying an Invoice System. Our specifications are written in TLA+, a formal specification language based on TLA (the Temporal Logic of Actions). We describe an animation language that allows us to validate our specifications. Finally, the specification, the validation and the verification of the invoice system are illustrated.
https://hal.inria.fr/inria-00098520
Contributeur : Publications Loria
<>
Soumis le : lundi 25 septembre 2006 - 17:03:06
Dernière modification le : mardi 24 avril 2018 - 13:34:44
Yassine Mokhtari. The invoice system problem in TLA+. International Workshop on Specification Techniques & Formal Methods, 1998, Nantes, France, 16 p, 1998. 〈inria-00098520〉
