Analyzing an Embedded Sensor with Timed Automata in Uppaal

Timothy Bourke 1, 2 Arcot Sowmya 3
1 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique de l'École normale supérieure, ENS Paris - École normale supérieure - Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Abstract : An infrared sensor is modeled and analyzed in Uppaal. The sensor typifies the sort of component that engineers regularly integrate into larger systems by writing interface hardware and software. In all, three main models are developed. For the first, the timing diagram of the sensor is interpreted and modeled as a timed safety automaton. This model serves as a specification for the complete system. A second model that emphasizes the separate roles of driver and sensor is then developed. It is validated against the timing diagram model using an existing construction that permits the verification of timed trace inclusion, for certain models, by reachability analysis (i.e., model checking). A transmission correctness property is also stated by means of an auxiliary automaton and shown to be satisfied by the model. A third model is created from an assembly language driver program, using a direct translation from the instruction set of a processor with simple timing behavior. This model is validated against the driver component of the second timing diagram model using the timed trace inclusion validation technique. While no pretense is made of providing a general means to verify systems, The approach and its limitations offer insight into the nature and challenges of programming in real time.
Type de document :
Article dans une revue
ACM Transactions on Embedded Computing Systems (TECS), ACM, 2013, 13 (3), pp.44-1--44-26. 〈10.1145/2539036.2539040〉
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00909062
Contributeur : Timothy Bourke <>
Soumis le : mardi 26 novembre 2013 - 13:44:21
Dernière modification le : mercredi 28 septembre 2016 - 14:01:57
Document(s) archivé(s) le : jeudi 27 février 2014 - 04:35:14

Fichier

tecs2012-accepted.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Timothy Bourke, Arcot Sowmya. Analyzing an Embedded Sensor with Timed Automata in Uppaal. ACM Transactions on Embedded Computing Systems (TECS), ACM, 2013, 13 (3), pp.44-1--44-26. 〈10.1145/2539036.2539040〉. 〈hal-00909062〉

Partager

Métriques

Consultations de la notice

349

Téléchargements de fichiers

445