FORMAL SPECIFICATION OF REACTIVE LOGICAL CONTROL DEVICES

摘要

In general case, logical control devices (LCDs) are asynchronous reactive embedded systems, carrying out control for several processes proceeding concurrently. Their design can begin from describing parallel algorithms for logical control (PALC). The paper presents two formal textual specification languages, which can be treated as textual descriptions of a control interpreted Petri net. On the other hand, the same languages can serve as design languages, related with parallel (concurrent) state machine models. A formal textual language LCA is suggested for representing any PALC as an unordered set of chains, which can be executed one by one or concurrently under the control of a mechanism of the Petri net type. As a design alternative, the symbolic rule-based specification of Petri net-based Logic Controllers (LCs) in the form of conditionals (decision rules) is considered. The behavioural specification can be formally transformed into the final specification (concurrent state machine model, easy for mapping in reconfigurable logic devices). Both behaviourally equivalent kinds of specification can be transformed into sequents, written in Gentzen logic, which are very suitable for direct mapping into Field Programmable Logic (FPL) implementations via modern HDLs, like VHDL.