A Logic of Actions and Its Application to the Development of Programmable Controllers

The objective of this book is a logic of actions (LA) . The central term in LA is processes . Elementary processes consist of actions which might occur or are forbidden . Modules , the formulas of LA, specify process sets. By assigning a timestamp to actions which designates their moment of occurrence, we extend LA by a time dimension, and call this extension timestamp logic of action (TiLA) . If a specification and a realization are given as LA or TiLA modules, we can prove in this logic whether the realization fulfills the specification. Petri netsare formalisms formodeling,analyzing, andsimulatingdynamicsystems.Activeandpassiveelements of systems are distinguished and related to each other in a Petri net model.With the aid ofmarkingthe passive elements, we specifystatesorsituationswhich hold for a modeled system. Sequentialoccurrencesof active elements which causestate transitionscan be used to specify process like information.Petri nets which are basically defined without time can be extended by an underlying time concept. Two examples for this aretimestamp netsandextended timestamp netswhere preconditions for the occurrence of state transitions only hold within atime window, and where this time window is defined with the aid oftimestampsassociated to partial markings.While LA modules can beimplementedwith the aid of simple Petri nets, we demonstrate how to implement TiLA modules with the aid of extended timestamp nets. The advantage of such implementations lies within simplified proving techniques. In order to demonstrate the applicability of TiLA (and LA), we conceptualize a software development process for programmable controllers which bases mainly on TiLA and which is structured as follows: with the aid of extended timestamp nets,dynamic modelsof the machine to be controlled are developed. By usingpictographs, we abstract from modeling details and give a better overview over the entire system. TiLA modules are used to specify thetechnical processesto be realized by the machine. A programming language notation of TiLA calledLAPsimplifies this task. The models of the uncontrolled machine and the technical processes are integrated into a model of thecontrolled machine. This model can be used tovirtually put the machine into operation. Finally, we cangenerate codefor programmable controllers out of the previous mentioned models. The software development process is examined with the aid of an example.During the machine is virtually put into operation, weverifyprocess-like and situation-like specifications. For process-like specifications on which we focus our considerations here, we prove that they aresoundandcompletewith respect to their specifications. Both terms are formally defined in LA and TiLA. Beside proving, we canvalidatethe previously developed models by simulating the model of the controlled machine.