Paper Info
Title
TEPE: a SysML language for time-constrained property modeling and formal verification
Abstract
Using UML or SysML models in a verification-centric method requires a property expression language, a formal semantics, and a tool. The paper introduces TEPE, a graphical TEmporal Property Expression language based on SysML parametric diagrams. TEPE enriches the expressiveness of other common property languages in particular with the notion of physical time and unordered signal reception. TEPE is further instantiated in the AVATAR real-time UML profile. TTool, an open-source toolkit, implements a press-button approach for the formal verification of AVATAR-TEPE properties with UPPAAL. An elevator system serves as example
Year
DOI
Venue
2011
10.1145/1921532.1921556
ACM SIGSOFT Software Engineering Notes
Keywords
Field
DocType
time-constrained property modeling,sysml parametric diagram,property expression language,avatar-tepe property,sysml language,graphical temporal property expression,elevator system,common property language,sysml model,avatar real-time uml profile,formal verification,formal semantics,real time
Common property,Programming language,Software engineering,Unified Modeling Language,Computer science,Parametric statistics,Systems Modeling Language,Avatar,Expressivity,Semantics of logic,Formal verification
Journal
Volume
Issue
Citations 
36
1
22
PageRank 
References 
Authors
1.14
7
3
Name
Order
Citations
PageRank
Daniel Knorreck1332.72
Ludovic Apvrille213622.23
Pierre de Saqui-Sannes313318.91