Specifying time-sensitive systems with TLA+
Résumé
We present a pattern-based method to express time specifications in the language TLA+. A real-time module RealTimeNew is introduced to encapsulate the definitions of commonly used time patterns. We present a general framework to differentiate the temporal characterizations from system functionality with time constraints. The temporal specification is concise and provably as a refinement of its corresponding functional description without time. The method ameliorates the usability of TLA+ in specifying and verifying time-sensitive systems. A case study is harnessed to illustrate and validate the approach.
Domaines
Génie logiciel [cs.SE]
Origine : Fichiers éditeurs autorisés sur une archive ouverte
Loading...