Abstract
A method to achieve executability of temporal logic specifications is restricting the interpretation of formulas over finite domains. This method was proven to be successful in designing testing tools used in industrial applications. However, the extension of the results of these tools to infinite, or just larger, domains, requires an adequate definition of a “finite-domain semantics”. Here we show the need for correcting previous semantics proposals, especially in the case of specifications of real-time systems which require the use of bounded temporal operators. We define a new semantics for the TRIO language, easily extendible to other linear metric temporal logic languages and show its adequateness on various examples.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R. Alur and T.A. Henzinger: Logics and Models of Real-Time: A Survey. Proc. of REX Workshop-Real-Time: Theory and Practice, Mook, The Netherlands, June 1991, LNCS 600, Springer Verlag, New York, 1992, pp. 74–106.
M. Basso, E. Ciapessoni, E. Crivelli, D. Mandrioli, A. Morzenti, P. San Pietro: Experimenting a Logic-based Approach to the Specification and Design of the Control System of a Pondage Power Plant. M. Wirsing (ed.), ICSE-17 Workshop on Formal Methods Application in Softw. Eng. Practice, Seattle, WA, April 1995.
E. Ciapessoni, E. Corsetti, A. Montanari, P. San Pietro: Embedding Time Granularity in a Logical Specification Language for Synchronous Real-Time Systems. Science of Computer Programming, 20 (1993), pp. 141–171, Elsevier Publishing, Amsterdam, 1993.
M. Felder, A. Morzenti: Validating real-time systems by history-checking TRIO specifications. ACM TOSEM-Transactions On Software Engineering and Methodologies, vol.3, n.4, October 1994
C. Ghezzi, D. Mandrioli, and A. Morzenti: TRIO, a logic language for executable specifications of real-time systems. Journal of Systems and Software 12, 2 (May 1990), 107–123.
A. Morzenti, and P. San Pietro: Object oriented logic specification of time-critical systems. ACM TOSEM, Vol. 3, n. 1, January 1994, pp. 56–98.
A. Morzenti, D. Mandrioli, and C. Ghezzi: A Model Parametric Real-Time Logic. ACM Transactions on Programming Languages and Systems 14, 4 (October 1992), 521–573.
D. Mandrioli, S. Morasca, A. Morzenti: Generating Test Cases for Real-Time Systems from Logic Specifications. ACM Trans. On Computer Systems, Vol. 13, No. 4, November 1995. pp.365–398.
S. Morasca, A. Morzenti, P. San Pietro: Generating Functional Test Cases in-the-large for Time-critical Systems from Logic-based Specifications. Proc. of ISSTA 1996, ACM-SIGSOFT International Symposium on Software Testing and Analysis, Jan. 1996, San Diego, CA.
A. Urquhart: Many valued Logic. D. Gabbay and F, Guenthner (eds), Handbook of Philosophical Logic, Vol. III, Kluwer, London, 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Coen-Porisini, A., Pradella, M., Pietro, P.S. (1998). A finite-domain semantics for testing temporal logic specifications. In: Ravn, A.P., Rischel, H. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 1998. Lecture Notes in Computer Science, vol 1486. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055335
Download citation
DOI: https://doi.org/10.1007/BFb0055335
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65003-4
Online ISBN: 978-3-540-49792-9
eBook Packages: Springer Book Archive