Title
Verification of external specifications of reactive systems
Abstract
External specification is currently approached by specification languages for describing and analyzing system requirements. The external specification can be defined during the early stages of the system development and can be very useful for: checking the class/system/subsystem requirements; checking the system composition; evaluating costs of reuse; defining validated reference requirements, histories, and traces for the final validation. The paper presents a collection of criteria in order to formally verify the external specification of reactive systems/subsystems. The verification criteria are grounded on the Tempo Reale object-oriented language (TROL) specification model for real-time systems. In TROL, the external specification is expressed in terms of ports and clauses with temporal constraints. The goal of the verification criteria presented is to check the completeness and consistency of the external specification with special attention to temporal constraints. These criteria can be applied to other real-time specification models and have been enforced in the tool object oriented machine state (TOOMS) tool. A practical example illustrates the verification process that embodies these criteria
Year
DOI
Venue
2000
10.1109/3468.895892
IEEE Transactions on Systems, Man, and Cybernetics, Part A
Keywords
Field
DocType
reactive system,real-time specification model,system development,system composition,specification model,specification language,external specification,temporal constraint,real-time system,verification criterion,consistency,object oriented languages,real time systems,formal specifications,formal specification,completeness,formal verification,history,reactive systems,object oriented language,message passing,object oriented
Specification language,Programming language,Computer science,Formal specification,Verification,Language Of Temporal Ordering Specification,Reactive system,System requirements specification,Software requirements specification,Formal verification
Journal
Volume
Issue
ISSN
30
6
1083-4427
Citations 
PageRank 
References 
5
0.56
28
Authors
3
Name
Order
Citations
PageRank
P. Bellini114413.33
Bruno, M.A.270.95
P. Nesi318625.96