A formal technique for the specification and verification of distributed systems and its application in manufacturing automation

Author

Fialho, S.V. ; Leão, J. L S ; Pedroza, A.C.P.

Author_Institution

Lab. de Engenharia de Comput. e Autom., Univ. Federal do Rio Grande do Norte, Natal, Brazil

Volume

1

fYear

1995

fDate

13-16 Aug 1995

Firstpage

27

Abstract

A methodology for specifying and verifying distributed systems is presented. The CRIS language, based on communicating extended finite state machines, is used in the specification of systems under development. The verification technique uses heuristic information on the specification objects (machine states, variables, FIFO queue contents and exchanged messages in the communication ports), for driving the reachability graph generation, used for checking properties of interest. A Flexible Assembly Cell (FAC) is used as a case study for a manufacturing system. Some results on the applicability of this approach to the FAC specification and verification are discussed

Keywords

assembling; distributed processing; finite state machines; flexible manufacturing systems; formal specification; formal verification; reachability analysis; CRIS language; FAC specification; FIFO queue contents; communicating extended finite state machines; distributed systems; exchanged messages; flexible assembly cell; formal technique; heuristic information; machine states; manufacturing automation; reachability graph generation; specification objects; verification technique; Assembly systems; Automata; Automatic control; Computer aided manufacturing; Control systems; Data flow computing; Distributed computing; Flexible manufacturing systems; Formal specifications; Manufacturing systems; Material storage;

fLanguage

English

Publisher

ieee

Conference_Titel

Circuits and Systems, 1995., Proceedings., Proceedings of the 38th Midwest Symposium on

Conference_Location

Rio de Janeiro

Print_ISBN

0-7803-2972-4

Type

conf

DOI

10.1109/MWSCAS.1995.504370

Filename

504370