Modelisation of timed automata in Coq
In: TACS 2001 : theoretical aspects of computer software (Sendai, 29-31 October 2001)Lecture notes in computer science :298-315
Konferenz
- print, 26 ref
Zugriff:
This paper presents the modelisation of a special class of timed automata, named p-automata in the proof assistant Coq. This work was performed in the framework of the CALIFE project1 which aims to build a general platform for specification, validation and test of critical algorithms involved in telecommunications. This paper does not contain new theoretical results but explains how to combine and adapt known techniques in order to build an environment dedicated to a class of problems. It emphasizes the specific features of Coq which have been used, in particular dependent types and tactics based on computational reflection.
Titel: |
Modelisation of timed automata in Coq
|
---|---|
Autor/in / Beteiligte Person: | PAULIN-MOHRING, Christine |
Link: | |
Quelle: | TACS 2001 : theoretical aspects of computer software (Sendai, 29-31 October 2001)Lecture notes in computer science :298-315 |
Veröffentlichung: | Berlin: Springer, 2001 |
Medientyp: | Konferenz |
Umfang: | print, 26 ref |
ISSN: | 0302-9743 (print) |
Schlagwort: |
|
Sonstiges: |
|