Verification Criteria for a Compositional Model for Reactive Systems

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by P. Bellini Articles by M.A. Bruno Articles by P. Nesi

Sixth IEEE International Conference on Complex Computer Systems (ICECCS'00)

Tokyo, Japan

September 11-September 15

ISBN: 0-7695-0583-X

	ASCII Text	x
	P. Bellini, M.A. Bruno, P. Nesi, "Verification Criteria for a Compositional Model for Reactive Systems," Engineering of Complex Computer Systems, IEEE International Conference on, pp. 0025, Sixth IEEE International Conference on Complex Computer Systems (ICECCS'00), 2000.

	BibTex	x
	@article{ 10.1109/ICECCS.2000.873925, author = {P. Bellini and M.A. Bruno and P. Nesi}, title = {Verification Criteria for a Compositional Model for Reactive Systems}, journal ={Engineering of Complex Computer Systems, IEEE International Conference on}, volume = {0}, year = {2000}, isbn = {0-7695-0583-X}, pages = {0025}, doi = {http://doi.ieeecomputersociety.org/10.1109/ICECCS.2000.873925}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Engineering of Complex Computer Systems, IEEE International Conference on TI - Verification Criteria for a Compositional Model for Reactive Systems SN - 0-7695-0583-X SP EP A1 - P. Bellini, A1 - M.A. Bruno, A1 - P. Nesi, PY - 2000 KW - formal specification; verification criteria; compositional model; reactive systems; system composition/decomposition; external interface; temporal constraint propagation; structural hierarchy; missing temporal constraints; graphical notation; TROL; object oriented real time language VL - 0 JA - Engineering of Complex Computer Systems, IEEE International Conference on ER -

P. Bellini, Dept. of Syst. & Inf., Firenze Univ., Italy

M.A. Bruno, Dept. of Syst. & Inf., Firenze Univ., Italy

P. Nesi, Dept. of Syst. & Inf., Firenze Univ., Italy

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICECCS.2000.873925

Abstract: System composition/decomposition has to be analyzed in terms of temporal constraints associated with the components' external interface. The analysis is focused on the propagation of temporal constraints along the structural hierarchy, thus showing that in many cases missing temporal constraints can be evaluated on the basis of the temporal constraints known. A set of criteria for the verification of the temporal constraints in a compositional model is presented. A specific graphical notation is proposed. The application of the criteria to a real problem is illustrated by using TROL, an object oriented real time language.

Index Terms:

formal specification; verification criteria; compositional model; reactive systems; system composition/decomposition; external interface; temporal constraint propagation; structural hierarchy; missing temporal constraints; graphical notation; TROL; object oriented real time language

Citation:

P. Bellini, M.A. Bruno, P. Nesi, "Verification Criteria for a Compositional Model for Reactive Systems," iceccs, pp.0025, Sixth IEEE International Conference on Complex Computer Systems (ICECCS'00), 2000

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.