Paper Info
Title
On the Semantics of Scenario-Based Specification Based on Timed Computational Tree Logic
Abstract
Scenario-based specifications have been widely used to specify the behavior of reactive systems in a visual and intuitive way. Timed Property Sequence Chart (TPSC) is a recently proposed scenario-based specification for specifying timing properties for real-time systems. However, there is currently no model checking tool available to verify timing properties specified by TPSC specifications. To mitigate this gap, this paper provides the semantics rules for TPSC by explicitly translating TPSC into Timed Computational Tree Logic (TCTL) that is a real time temporal logic. Two kinds of rules are defined: basic and compositional rules. Basic rules discuss how to translate a single message in a TPSC specification into a TCTL formula, while compositional rules show how to compose these basic TCTL formulas according to compositional operators. The classification of basic and compositional rules makes our translations more efficient. The translation process is illustrated by a case study. The translating correctness is also proved by the practical measurement of real-time specification patterns. The work described here opens an indirect way to model checking real-time requirements represented in TPSC specifications by translating TPSC specifications into TCTL formulas.
Year
DOI
Venue
2013
10.1109/ASWEC.2013.11
Australian Software Engineering Conference
Keywords
Field
DocType
real-time requirement,real-time specification pattern,basic rule,basic tctl formula,compositional operator,tctl formula,compositional rule,timing property,tpsc specification,timed computational tree logic,scenario-based specification,real time system,semantics,real time systems,temporal logic,model checking,formal specification
Computation tree logic,Programming language,Model checking,Computer science,Correctness,Theoretical computer science,Real-time operating system,Formal specification,Temporal logic,Reactive system,Semantics
Conference
ISSN
Citations 
PageRank 
1530-0803
0
0.34
References 
Authors
23
2
Name
Order
Citations
PageRank
Wenrui Li1588.98
Pengcheng Zhang24010.97