The invoice system problem in TLA+

Yassine Mokhtari 1
1 MODEL - MODEL (Méthodes formelles et applications)
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Type de document :
Communication dans un congrès
International Workshop on Specification Techniques & Formal Methods, 1998, Nantes, France, 16 p, 1998
Liste complète des métadonnées

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

Identifiants

  • HAL Id : inria-00098520, version 1

Collections

Citation

Yassine Mokhtari. The invoice system problem in TLA+. International Workshop on Specification Techniques & Formal Methods, 1998, Nantes, France, 16 p, 1998. 〈inria-00098520〉

Partager

Métriques

Consultations de la notice

116