| Reference : A Model-Driven Approach to Offline Trace Checking of Temporal Properties with OCL |
| Reports : Internal report | |||
| Engineering, computing & technology : Computer science | |||
| http://hdl.handle.net/10993/16112 | |||
| A Model-Driven Approach to Offline Trace Checking of Temporal Properties with OCL | |
| English | |
Dou, Wei  [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >] | |
| Bianculli, Domenico [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >] | |
| Briand, Lionel [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > > ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)] | |
| 20-Mar-2014 | |
| SnT Centre - University of Luxembourg | |
| 978-2-87971-125-6 | |
| SnT-TR-2014-5 | |
| [en] trace checking ; temporal properties ; property specification patterns ; model-driven engineering ; OCL | |
| [en] Offline trace checking is a procedure for evaluating requirements over
a log of events produced by a system. The goal of this paper is to present a practical and scalable solution for the offline checking of the temporal requirements of a system, which can be used in contexts where model-driven engineering is already a practice, where temporal specifications should be written in a domain-specific language not requiring a strong mathematical background, and where relying on standards and industry-strength tools for property checking is a fundamental prerequisite. The main contributions are: the TemPsy language, a domain-specific specification language based on common property specification patterns, and extended with new constructs; a model-driven offline trace checking procedure based on the mapping of requirements written in TemPsy into OCL (Object Constraint Language) constraints on a conceptual model on execution traces, which can be evaluated using an OCL checker; the implementation of this trace checking procedure in the TemPsy-Check tool; the evaluation of the scalability of TemPsy-Check and its comparison to a state-of-the-art alternative technology. The proposed approach has been applied to a case study developed in collaboration with a public service organization, active in the domain of business process modeling for eGovernment. | |
| Interdisciplinary Centre for Security, Reliability and Trust (SnT) > Software Verification and Validation Lab (SVV Lab) | |
| Fonds National de la Recherche - FnR | |
| http://hdl.handle.net/10993/16112 |
| File(s) associated to this reference | ||||||||||||||
|
Fulltext file(s):
| ||||||||||||||
All documents in ORBilu are protected by a user license.
