Affordable Access

Access to the full text

Polychronous automata and their use for formal validation of AADL models

Authors
  • Gautier, Thierry1
  • Guy, Clément1
  • Honorat, Alexandre1
  • Le Guernic, Paul1
  • Talpin, Jean-Pierre1
  • Besnard, Loïc2
  • 1 Univ. Rennes, Inria, Rennes-Bretagne-Atlantique Research Centre, Rennes, F-35000, France , Rennes (France)
  • 2 Univ. Rennes, CNRS, IRISA, Rennes, F-35000, France , Rennes (France)
Type
Published Article
Journal
Frontiers of Computer Science
Publisher
Higher Education Press
Publication Date
May 27, 2019
Volume
13
Issue
4
Pages
677–697
Identifiers
DOI: 10.1007/s11704-017-6134-5
Source
Springer Nature
Keywords
License
Yellow

Abstract

This paper investigates how state diagrams can be best represented in the polychronous model of computation (MoC) and proposes to use this model for code validation of behavior specifications in Architecture Analysis & Design Language (AADL). In this relational MoC, the basic objects are signals, which are related through dataflow equations. Signals are associated with logical clocks, which provide the capability to describe systems in which components obey multiple clock rates. We propose a model of finite-state automata, called polychronous automata, which is based on clock relationships. A specificity of this model is that an automaton is submitted to clock constraints, which allows one to specify a wide range of control-related configurations, being either reactive or restrictive with respect to their control environment. A semantic model is defined for these polychronous automata, which relies on boolean algebra of clocks. Based on a previously defined modeling method for AADL software architectures using the polychronous MoC, the proposed model is used as a formal model for the AADL behavior annex. This is illustrated with a case study involving an adaptive cruise control system.

Report this publication

Statistics

Seen <100 times