TILCO Temporal Logic for Real-Time Systems Implementation in C++.
作者： Davide Rogai , Pierfrancesco Bellini , Andrea Giotti , Paolo Nesi
DOI:
关键词:
摘要: Temporal logics are capable to describe temporal constraints among events and actions, as invariance, precedence, periodicity, repeated occurrences, liveness safety conditions. They typically used specify verify properties in the requirement analysis, system behavior that can be verified via property proof. Operational approaches have a state-based semantics which is many cases preferred at denotational for their immediate interpretation automatic conversion into programming language. In fact, implementation of real-time systems traditional languages still used. this paper, an integrated development environment implement based on integration TILCO logic C++ presented. The execution Logic specifications manage concurrent, behavioral requirements application Real-Time. Results about new model
参考文章(11)
Mordechai Ben-Ari, Mathematical Logic for Computer Science ,(1993)
Tobias Nipkow, Lawrence C. Paulson, Isabelle: A Generic Theorem Prover ,(1994)
P. Bellini, R. Mattolini, P. Nesi, Temporal logics for real-time system specification ACM Computing Surveys. ,vol. 32, pp. 12- 42 ,(2000) , 10.1145/349194.349197
R. Mattolini, P. Nesi, An interval logic for real-time system specification IEEE Transactions on Software Engineering. ,vol. 27, pp. 208- 227 ,(2001) , 10.1109/32.910858
Giacomo Bucci, Maurizio Campanai, Paolo Nesi, Tools for specifying real-time systems Real-time Systems. ,vol. 8, pp. 117- 172 ,(1995) , 10.1007/BF01094341
Ron Koymans, Specifying Message Passing and Time-Critical Systems with Temporal Logic ,(1992)
Michael Fisher, Richard Owens, An Introduction to Executable Modal and Temporal Logics international joint conference on artificial intelligence. pp. 1- 20 ,(1993) , 10.1007/3-540-58976-7_1
P. Bellini, A. Giotti, P. Nesi, Execution of TILCO temporal logic specifications international conference on engineering of complex computer systems. pp. 78- 87 ,(2002) , 10.1109/ICECCS.2002.1181500
Miguel Felder, Angelo Morzenti, Validating real-time systems by history-checking TRIO specifications ACM Transactions on Software Engineering and Methodology. ,vol. 3, pp. 308- 339 ,(1994) , 10.1145/201024.201034
James F. Allen, George Ferguson, Actions and Events in Interval Temporal Logic Journal of Logic and Computation. ,vol. 4, pp. 531- 579 ,(1994) , 10.1007/978-0-585-28322-7_7