Modeling and analysis of complex computer systems-the MTCCS approach

Author

Toetenel, Hans ; Spelberg, Ronald Lutje ; Stuurman, Sylvia ; van Katwijk, Jan

Author_Institution

Fac. of Math. & Inf., Delft Univ. of Technol., Netherlands

fYear

1996

fDate

21-25 Oct 1996

Firstpage

423

Lastpage

430

Abstract

The paper presents results from work in progress on finding a method for formal specification and verification of real time concurrent systems that incorporate a non trivial data component. We have extended Timed CCS, a timed CCS variant with a model oriented data language based on VDM. The semantics of the extension, called MTCCS is expressed in a combination of denotational and operational style. We show how verification of temporal logic properties based on symbolic model checking can be made possible for such a combination notation

Keywords

calculus of communicating systems; formal specification; parallel programming; program verification; real-time systems; specification languages; temporal logic; MTCCS approach; Model Oriented Timed Calculus of Communicating Systems; Timed CCS; VDM; combination notation; complex computer systems analysis; complex computer systems modeling; formal specification; model oriented data language; non trivial data component; operational style; real time concurrent systems; specification language; symbolic model checking; temporal logic properties; verification; work in progress; Carbon capture and storage; Concurrent computing; Distributed computing; Formal specifications; Informatics; Logic; Mathematics; Paper technology; Protocols; Real time systems;

fLanguage

English

Publisher

ieee

Conference_Titel

Engineering of Complex Computer Systems, 1996. Proceedings., Second IEEE International Conference on

Conference_Location

Montreal, Que.

Print_ISBN

0-8186-7614-0

Type

conf

DOI

10.1109/ICECCS.1996.558488

Filename

558488