TEPE: a SysML language for time-constrained property modeling and formal verification
Résumé
Using UML or SysML models in a verification-centric method requires a property expression language, a formal se- mantics, and a tool. The paper introduces TEPE, a graphi- cal TEmporal Property Expression language based on SysML parametric diagrams. TEPE enriches the expressiveness of other common property languages in particular with the no- tion 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 ap- proach for the formal verification of AVATAR-TEPE proper- ties with UPPAAL. An elevator system serves as example.
Domaines
Génie logiciel [cs.SE]
Origine : Fichiers éditeurs autorisés sur une archive ouverte
Loading...