UNSPECIFIED (2004) Specifying and verifying partial order properties using template MSCs. In: 7th International Conference on Foundations of Software Science and Computation Structures, MAR 30-APR 02, 2004, Barcelona, SPAIN.

Full text not available from this repository.

Abstract

Message sequence charts (MSC) are a graphical language for the description of communication scenarios between asynchronous processes. Our starting point is to model systems using an assume-guarantee formalism, in the style of LSCs and Triggered MSCs. We enrich MSCs with the possibility of using gaps (template MSC), and show their ex-pressivity. This formalism also allows to express logical formulas. We analyze the model-checking problem, whose complexity is linear in the size of the system, and ranges from PTIME to EXPSPACE in the size of the template formula.

Item Type:	Conference Item (UNSPECIFIED)
Subjects:	Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Series Name:	LECTURE NOTES IN COMPUTER SCIENCE
Journal or Publication Title:	FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PROCEEDINGS
Publisher:	SPRINGER-VERLAG BERLIN
ISBN:	3-540-21298-1
ISSN:	0302-9743
Editor:	Walukiewicz, I
Date:	2004
Volume:	2987
Number of Pages:	16
Page Range:	pp. 195-210
Publication Status:	Published
Title of Event:	7th International Conference on Foundations of Software Science and Computation Structures
Location of Event:	Barcelona, SPAIN
Date(s) of Event:	MAR 30-APR 02, 2004
URI:	http://wrap.warwick.ac.uk/id/eprint/8450

Data sourced from Thomson Reuters' Web of Knowledge

Request changes to a record

Actions (login required)

View Item