Hybrid Input Output Automata for composable conveyor systems

We present Hybrid Input/Output Automata (HIOA) models as a basis for the design and analysis of a class of composable conveyor systems. These conveyor systems are realized by composing instances of two kinds of units, namely segments and turns. A microcontroller, which is physically wired to the sensors and actuators on the unit, regulates the local operations at the unit level. Microcontrollers that regulate physically adjacent units interact with each other over wireless links. Our HIOA models capture the continuous dynamics of obAcircnot jects moving on a unit and the discrete sequence of interactions that coordinate operations across adjacent units. Coordination messages exchange status information and transfer objects from one unit to another. We use two layers of automata. The first, called RC (Route Control), maintains system-wide routes over which objects move in the conveyor systems. This automaton is common to all units. The second automaton, called TC (Traffic Control), interacts with the local environment. Each unit has a specialized TC automaton depending on whether it is a segment or a turn. The TC automata in physically adjacent units exchange Red and Green signals to regulate the movement of objects from one unit to the other. By composing instances of these automata models, we achieve system-level models for the conveyor systems. Using the formal reasoning mechanisms in HIOA theory, we expect to establish properties of the composed conveyor systems. For example, as preliminary results, we can show that the Route Control Protocol is self-stabilizing. We can also show that the signaling mechanism in the TC automata help to maintain spatial/temporal constraints, such as minimum gap between objects moving on the conveyor system. As our next step, we are working on specifying a third automaton, called MP that is an implementation of the TC and RC automata on a microcontroller platform. We aim to shown that if the execution of MP satisfies certain tempora- l constraints, then the composed conveyor systems are correct by construction and deliver the properties that we can deduce via an analysis of the HIOA models of composed conveyor systems.