by Maurice ter Beek, Josep Carmona and Jetty Kleijn
Society is still trying to catch up with technology in the wake of the digital revolution of the last twenty years. Current systems need to be both heterogeneous and able to deal with enormous volumes of data coming from uncertain environments; consequently it is essential to be able to automatically assess the correctness of interactions. To guarantee that a system of systems, comprising a conglomerate of cooperating reactive components, can be trusted, and that the system as a whole behaves as intended, requires a thorough understanding of its communication behaviour. Once local interactions are identified, abstractions can support the identification of incompatibility of systems that should cooperate within a larger system.
In an increasingly smart, connected world in which digital communications outnumber all other forms of communication, it is important to understand the complex underlying interconnections in the numerous systems of systems that govern our daily life. This requires a deep understanding of all kinds of different communication and collaboration strategies (e.g. client-server, peer-to-peer and master-slave) used in embedded or multi-component systems and the risk of failures they entail (e.g. message loss and deadlocks can have severe repercussions on reliability, safety and security).
A project involving ISTI-CNR and Leiden University (the Netherlands) considers fundamental notions paramount for the development of correct-by-construction multi-component systems. Basic building blocks are reactive components that interact with each other via shared (external) actions; internal actions are never shared. External actions can be input or output to the components to which they belong. Components can be added in different phases of construction allowing for hierarchically composed systems of systems. To establish that components within a system or a system and its environment always interact correctly, a concept of compatibility is needed. Compatibility represents an aspect of successful communication behaviour, a necessary ingredient for the correctness of a distributed system. Compatibility failures detected in a system model may reveal important problems in the design of one or more of its components that must be repaired before implementation.
In [1] a definition is given for compatibility of two components that should engage in a dialogue free from message loss and deadlocks. Message loss occurs when one component sends a message that cannot be received as input by another component, whereas deadlock occurs when a component is indefinitely waiting for a message that never arrives. The aim of the ideas developed in [1] is to provide a formal framework for the synthesis of asynchronous circuits and embedded systems. There the approach is restricted to two components and a closed environment, i.e. all input (output) actions of one component are output (input) actions of the other component.
In [2] this approach is generalized to distributed systems which consist of several components, and within which communication and interaction may take place between more than two components at the same time (e.g. broadcasting). These multi-component systems are represented by team automata [3], originally introduced to model groupware systems. Team automata represent a useful model to specify intended behaviour and have been shown to form a suitable formal framework for lifting the concept of compatibility to a multi-component setting. They resemble the well-known I/O automata in their distinction between input (passive), output (active) and internal (private) actions, but an important difference is that team automata impose fewer a priori restrictions on the role of the actions and the interactions between the components [3]. In [2] emphasis is on team automata with interactions based on mandatory synchronized execution of common actions.
Together with the Universitat Politècnica de Catalunya (Barcelona, Spain) we plan to continue the approach of [2] by investigating other composition strategies and, in particular, focusing on how to handle compositions based on master-slave collaborations. In such collaborations, input (the slave) is driven by output (the master) under different assumptions ranging from slaves that cannot proceed on their own to masters that should always be followed by slaves. Thus we address questions such as “how is compatibility affected when slaves are added?” and “in what way does compatibility depend on the collaboration among slaves?” Practical solutions to these answers may have strong impacts in various fields, such as services computing and security.
Composition and modularity are common in modern system design. So compatibility checks considering varying strategies significantly aid the development of correct-by-construction multi-component systems. Hence the ideas in this project should serve the development of techniques supporting the design, analysis and verification of systems of systems.
References:
[1] J. Carmona and J. Cortadella: “Input/Output Compatibility of Reactive Systems”, Formal Methods in Computer-Aided Design, LNCS 2517 (2002) 360-377
[2] J. Carmona and J. Kleijn: “Compatibility in a multi-component environment”, Theoretical Computer Science 484 (2013) 1-15
[3] M.H. ter Beek and J. Kleijn: “Modularity for Teams of I/O Automata”, Information Processing Letters 95, 5 (2005) 487-495
Please contact:
Maurice ter Beek
ISTI-CNR, Italy
E-mail:
