The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.12 - December (2005 vol.31)
pp: 1028-1041
ABSTRACT
A major obstacle in the technology-transfer agenda of behavioral analysis and design methods is the need for logics or automata to express properties for control-intensive systems. Interaction-modeling notations may offer a replacement or a complement, with a practitioner-appealing and lightweight flavor, due partly to the subspecification of intended behavior by means of scenarios. We propose a novel approach consisting of engineering a new formal notation of this sort based on a simple compact declarative semantics: VTS (Visual Timed event Scenarios). Scenarios represent event patterns, graphically depicting conditions over traces. They predicate general system events and provide features to describe complex properties not expressible with MSC-like notations. The underlying formalism supports partial orders and real-time constraints. The problem of checking whether a timed-automaton model has a matching trace is proven decidable. On top of this kernel, we introduce a notation to state properties over all system traces: conditional scenarios, allowing engineers to describe uniquely rich connections between antecedent and consequent portions of the scenario. An undecidability result is presented for the general case of the model-checking problem over dense-time domains, to later identify a decidable—yet practically relevant—subclass, where verification is solvable by generating antiscenarios expressed in the VTS{\hbox{-}}{\rm kernel} notation.
INDEX TERMS
Index Terms- Requirements/specifications, model checking, formal methods, scenario-based verification.
CITATION
Nicolas Kicillof, Alfredo Olivero, "A Scenario-Matching Approach to the Description and Model Checking of Real-Time Properties", IEEE Transactions on Software Engineering, vol.31, no. 12, pp. 1028-1041, December 2005, doi:10.1109/TSE.2005.131
22 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool