Specification language for automatа-based objects cooperation

Automata-based programming is a programming paradigm that has been successfully used in the development of reactive systems, distributed control systems, and various mission-critical applications where the ability to verify the compliance of a real system with its model given in the form of specifications is critical. The traditional testing of such systems can be difficult; thus, more advanced verification tools are required to increase confidence in the reliability of real systems. The previously proposed language for the specification of the Cooperative Interaction of Automata-based Objects (CIAO) was successfully used to develop several different reactive systems as a result of which a number of shortcomings were identified and eliminated in the new version of CIAO v.3. This new version of the language was developed for the automatic verification of automata-based programs according to the formal specifications of a certain class of real-time systems. Three innovations distinguish CIAO v.3 from previous versions. First, an explicit distinction between automata classes and automaton objects as instances of these classes. Second, we specify the binding of automaton objects through interfaces using a connection scheme. Third, we describe the semantics of the behavior of a system of interacting automaton objects using a semantic graph. This paper presents the main concepts of the new language version including the abstract syntax, operational semantics, and metamodel. The third version of the CIAO language naturally includes almost all the advantages of object-oriented programming into the paradigm of automata programming. The connection of automaton objects through the corresponding interfaces is arbitrarily reflected by the connection scheme. A semantic graph describing the semantics of the behavior of the automata-based program is used to implement automatic verification with respect to formal specifications.