Record Details

Checking conformance for time-constrained scenario-based specifications

DSpace at IIT Bombay

View Archive Info
 
 
Field Value
 
Title Checking conformance for time-constrained scenario-based specifications
 
Creator AKSHAY, S
GASTIN, P
MUKUND, M
KUMAR, KN
 
Subject MESSAGE SEQUENCE CHARTS
MODEL CHECKING
PETRI NETS
AUTOMATA
UNFOLDINGS
MSC graphs
Timed automata
Model checking
 
Description We consider the problem of model checking message-passing systems with real-time requirements. As behavioral specifications, we use message sequence charts (MSCs) annotated with timing constraints. Our system model is a network of communicating finite state machines with local clocks, whose global behavior can be regarded as a timed automaton. Our goal is to verify that all timed behaviors exhibited by the system conform to the timing constraints imposed by the specification. In general, this corresponds to checking inclusion for timed languages, which is an undecidable problem even for timed regular languages. However, we show that we can translate regular collections of time-constrained MSCs into a special class of event-clock automata that can be determinized and complemented, thus permitting an algorithmic solution to the model checking/conformance problem. (C) 2015 Elsevier B.V. All rights reserved.
 
Publisher ELSEVIER SCIENCE BV
 
Date 2016-01-15T05:51:01Z
2016-01-15T05:51:01Z
2015
 
Type Article
 
Identifier THEORETICAL COMPUTER SCIENCE, 594,24-43
0304-3975
1879-2294
http://dx.doi.org/10.1016/j.tcs.2015.03.030
http://dspace.library.iitb.ac.in/jspui/handle/100/17859
 
Language en