Validating real-time systems by history-checking TRIO specifications

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Validating real-time systems by history-checking TRIO specifications

Full text

Pdf (1.17 MB)

Source

International Conference on Software Engineering archive
Proceedings of the 14th international conference on Software engineering table of contents

Melbourne, Australia

Pages: 199 - 211

Year of Publication: 1992

ISBN:0-89791-504-6

Authors

Miguel Felder
Angelo Morzenti

Sponsors

IEEE-CS\TCSE : TC on Software Engineering
ACS :
IEA :
IREE :
SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 8, Citation Count: 7

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/143062.143115 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Alfred V. Aho , John E. Hopcroft , Jeffrey Ullman , J. D. Ullman , J. E. Hopcroft, Data Structures and Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1983
	2	Alur, R. and Henzinger, T.A. RealTime Logics: complexity and expressiveness, In 5th IEEE LICS 90, 1990.
	3	Peter B. Andrews, An introduction to mathematical logic and type theory: to truth through proof, Academic Press Professional, Inc., San Diego, CA, 1986
	4	Burch, J., Clarke, E., Millan, K.L.M., Dill, D., and Hwang, H. Symbolic Model Checking: 10^2O states and Beyond. In 5th Annual Symposium on Logic in Comp. Science, IEEE, July 1990, pp. 428-439.
	5	Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
	6	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
	7	Ghezzi, C., Mandrioli, D., and Morzenti, A. TRIO, a logic language for executable specifications of realtime systems . In 10th FrenchTunisian Seminar on Computer Science, Tunis, May 1989., pp. 322-349.
	8	C. Ghezzi , D. Mandrioli , A. Morzenti, TRIO: A logic language for executable specifications of real-time systems, Journal of Systems and Software, v.12 n.2, p.107-123, May 1990 [doi>10.1016/0164-1212(90)90074-V]
	9	Carlo Ghezzi , Mehdi Jazayeri , Dino Mandrioli, Fundamentals of software engineering, Prentice-Hall, Inc., Upper Saddle River, NJ, 1991
	10	Kemmerer, R.A. Testing Formal Specifications to Detect Design Errors. IEEE Transactions on Software Engineering (January 1985).
	11	Koymans, R. Specifying Message Passing and Time Critical Systems with Temporal Logic, Ph.D. dissertation, Eindhoven University of Technology., 1989.
	12	Fred Kröger, Temporal logic of programs, Springer-Verlag New York, Inc., New York, NY, 1987
	13	Zohar Manna , Pierre Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.68-93, Jan. 1984 [doi>10.1145/357233.357237]
	14	Elliott Mendelson, Introduction to mathematical logic (3rd ed.), Wadsworth Publ. Co., Belmont, CA, 1987
	15	Morzenti, A., Ratto, E., Roncato, M., and Zoccolante, L. TRIO: a Logic Formalism for the Specification of Real Time Systems. In Euromicro Workshop on Real Time, IEEE, Como, Italy, 1989.
	16	Morzenti, A. and SanPietro, P. TRIO+ an Object Oriented Logic Specification Language. Tech. Rept. Research Report, ENELCRA , in Italian, January , 1990.
	17	Angelo Morzenti , Pierluigi San Pietro, An Object-Oriented Logic Language for Modular System Specification, Proceedings of the European Conference on Object-Oriented Programming, p.39-58, July 15-19, 1991
	18	Angelo Morzenti , Dino Mandrioli , Carlo Ghezzi, A model parametric real-time logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.14 n.4, p.521-573, Oct. 1992 [doi>10.1145/133233.129397]
	19	Jonathan S. Ostroff, Temporal logic for real time systems, John Wiley & Sons, Inc., New York, NY, 1989
	20	Pnueli, A. The temporal semantics of concurrent programs . Theoretical Computer Science , 13 (1981), North Holland Publishing Company.
	21	Franco P. Preparata , Michael I. Shamos, Computational geometry: an introduction, Springer-Verlag New York, Inc., New York, NY, 1985
	22	Smullian, R.M. First order Logic, Springer Verlag (1968).
	23	Niklaus Wirth, Toward a discipline of real-time programming, Communications of the ACM, v.20 n.8, p.577-583, Aug. 1977 [doi>10.1145/359763.359798]

CITED BY 7

	Farn Wang , Aloysius K. Mok , E. Allen Emerson, Distributed real-time system specification and verification in APTL, ACM Transactions on Software Engineering and Methodology (TOSEM), v.2 n.4, p.346-378, Oct. 1993
	Angelo Morzenti , Pierluigi San Pietro, Object-oriented logical specification of time-critical systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.1, p.56-98, Jan. 1994
	P. Bellini , R. Mattolini , P. Nesi, Temporal logics for real-time system specification, ACM Computing Surveys (CSUR), v.32 n.1, p.12-42, March 2000
	Miguel Felder , Angelo Morzenti, Validating real-time systems by history-checking TRIO specifications, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.4, p.308-339, Oct. 1994
	Jonathan E. Cook , Alexander L. Wolf, Software process validation: quantitatively measuring the correspondence of a process to a model, ACM Transactions on Software Engineering and Methodology (TOSEM), v.8 n.2, p.147-176, April 1999
	M. Felder , D. Mandrioli , A. Morzenti, Proving Properties of Real-Time Systems Through Logical Specifications and Petri Net Models, IEEE Transactions on Software Engineering, v.20 n.2, p.127-141, February 1994
	Riccardo Mattolini , Paolo Nesi, An Interval Logic for Real-Time System Specification, IEEE Transactions on Software Engineering, v.27 n.3, p.208-227, March 2001