Abstract
Reactive systems, such as operating systems or elevator control systems, are systems that ideally never terminate and are intended to maintain some interaction with their environment. Temporal logic is one of the methods for formal specification descriptions of reactive systems. By describing the formal specifications of reactive systems we can check the consistency of the specifications and whether they contain defects. By using a synthesis algorithm we also obtain reactive system programs from the formal specifications and prevent programming bugs. Therefore, it is important to describe reactive system formal specifications to secure reactive system programs. However, it is difficult to describe realizable reactive system specifications and it is important to revise unrealizable reactive system specifications into realizable reactive system specifications. In previous research, three properties have been introduced into unrealizable reactive system specifications. By using these properties, we can acquire more detailed information about the cause of the defects of unrealizable reactive system specifications in the specification description process. In this paper, we propose decision procedures that judge whether a reactive system specification has these properties. We also prove the soundness and completeness of these procedures.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Pnueli, A.: The Temporal Logic in Programs. In: Proc. 18th Ann. IEEE Symp. on Foundations of Computer Science, pp. 46–57 (1977)
Emerson, E.A.: Temporal and Modal Logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. North-Holland, Amsterdam (1990)
Abadi, M., Lamport, L., Wolper, P.: Realizable and Unrealizable Specifications of Reactive Systems. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 1–17. Springer, Heidelberg (1989)
Pnueli, A., Rosner, R.: On the Synthesis of a Reactive Module. In: Proc. 16th Ann. ACM Symp. on the Principle of Programming Languages, pp. 179–190 (1989)
Manna, Z., Wolper, P.: Synthesis of Communicating processes from Temporal Logic Specifications. ACM Trans. Programming Languages and Systems 6(1), 68–93 (1984)
Emerson, E.A., Clarke, E.M.: Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. Sci. Comput. Programming 2, 241–266 (1982)
Wolper, P.: Temporal Logic can be more expressive. Informaition and Control 56, 72–93 (1983)
Pnueli, A., Rosner, R.: On the Synthesis of an Asynchronous Reactive Module. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 652–671. Springer, Heidelberg (1989)
Anuchitanukul, A., Manna, Z.: Realizability and Synthesis of Reactive Modules. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 156–168. Springer, Heidelberg (1994)
Vardi, M.Y.: An Automata-Theoretic Approach to Fair Realizability and Synthesis. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 267–278. Springer, Heidelberg (1995)
van der Meyden, R., Vardi, M.Y.: Synthesis from Knowledge-Based Specifications. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 34–49. Springer, Heidelberg (1998)
Mori, R., Yonezaki, N.: Several Realizability Concepts in Reactive Objects. In: Information Modeling and Knowledge Bases. IOS Press, Amsterdam (1993)
Mori, R., Yonezaki, Y.: Derivation of the Input Conditional Formula from a Reactive System Specification in Temporal Logic. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 567–582. Springer, Heidelberg (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yoshiura, N. (2004). Decision Procedures for Several Properties of Reactive System Specifications. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds) Software Security - Theories and Systems. ISSS 2003. Lecture Notes in Computer Science, vol 3233. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-37621-7_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-37621-7_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23635-1
Online ISBN: 978-3-540-37621-7
eBook Packages: Springer Book Archive