Title :
A state based language for discrete control and the verification of its programs
Author :
Leão, J. L S ; Fialho, S.V. ; Pedroza, A.C.P.
Author_Institution :
PEE-COPPE/Federal Univ. of Rio de Janeiro, Brazil
Abstract :
The CRIS language and a related temporal logic proof scheme are presented. The CRIS language, based on an extended finite-state machine model, is applied to the formal specification and implementation of logic control problems and to discrete event control in general. The associated temporal logic framework allows the verification of properties of programs written in CRIS. An example, the control of a jacketed reactor, is presented, which shows the applicability of CRIS language for logic control problems and its related temporal logic framework as a tool for proving program properties
Keywords :
finite automata; formal languages; logic programming; programmable controllers; CRIS language; discrete control; discrete event control; extended finite-state machine model; formal specification; jacketed reactor; logic control problems; program properties; state based language; temporal logic proof scheme; verification; Automata; Bipartite graph; Delay; Formal specifications; Inductors; Logic; Size control;
Conference_Titel :
Circuits and Systems, 1989., IEEE International Symposium on
Conference_Location :
Portland, OR
DOI :
10.1109/ISCAS.1989.100402
