Compositional approach to the development of reactive algorithms
- PDF / 255,325 Bytes
- 11 Pages / 594 x 792 pts Page_size
- 53 Downloads / 176 Views
COMPOSITIONAL APPROACH TO THE DEVELOPMENT OF REACTIVE ALGORITHMS UDC 519.713.1
A. N. Chebotarev
Abstract. A method is proposed for the development of complex finite state machines (FSMs) from their compositional specifications in the logical language L. A compositional specification of an FSM consists of specifications of its component modules and interconnections between them. The FSM synthesized is obtained by combining the state transition graphs of the modules synthesized from their specifications. Keywords: module of an algorithm, compositional specification, language L, S-FSM, w-word, operation of connecting modules, designation of a state. INTRODUCTION The considered process of developing a reactive algorithm lies in creating a formal specification of requirements on its behavior and automatically transforming such a (usually declarative) specification into an imperative (procedural) representation of the algorithm. A specification of requirements on the functioning of an algorithm is a set of statements that are written in a formal language and must be true at every instant of the functioning of the algorithm. In the approach being used, such a specification consists of two components, namely, a specification of the control component of the algorithm and a specification of its operational component. The operational component of an algorithm is implemented in the form of a rather regular (software or hardware) structure and, therefore, problems of specifying and implementing this component are essentially simpler than similar problems for its control component, and it is the latter problems to which the present work is devoted. Since the development of the control component of an algorithm is carried out with allowance made for constraints determined by its operational component and environment, these constraints must also be specified to optimize the control component. Algorithms of small systems functioning under a rather simple control can be specified by one collection of requirements, i.e., a collection of invariants that must hold at any moment of system operation. However, the specification of behaviors of complex systems, in particular, systems whose functioning can significantly change with time by one collection of requirements is incomparably more complicated. With increasing the complexity of the algorithm being specified, the number of invariants and complexity of formulas expressing them increase, which leads to a nonlinear growth of the complexity of its specification depending on the complexity of the algorithm. As is obvious, the probability of occurrence of an error in such a specification also considerably increases, and, moreover, the algorithm synthesis time exponentially dependent on the size of the specification may inadmissibly increase. Therefore, it makes sense to divide a specification into several fragments specifying separate parts of the algorithm of system operation that are called modules and are combined into one algorithm at the level of the state transition graphs of the
Data Loading...
