Abstract
We present a complete solution of the RPC-Memory Specification Problem, by applying a constraint-oriented state-based proof methodology for concurrent software systems. Our methodolgy exploits compositionality and abstraction for the reduction of the verification problem under investigation. Formal basis for this methodology are Modal Transition Systems allowing loose state-based specifications, which can be refined by successively adding constraints. Key concepts of our method are projective views, separation of proof obligations, Skolemization and abstraction. Central to the method is the use of Parametrized Modal Transition Systems. The method extends elegantly to real-time systems.
This author has been partially supported by the European Communities under CON-CUR2, BRA 7166.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, T.A. Henzinger, M.Y. Vardi. Parametric real-time reasoning. Proc. 25th STOC, ACM Press 1993, pp. 592–601.
M. Broy, L. Lamport. The RPC-Memory Specification Problem. This volume.
E. Clarke, E.A. Emerson, A.P. Sistla. Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications: A Practical Approach. In Proceedings 10th POPL'83, 1983
K. Čerāns, J.C. Godsken, K.G. Larsen. Timed Modal Specification — Theory and Tools. in: C. Courcoubetis (Ed.), Proc. 5th Int. Conf. on Computer Aided Verification (CAV '93), Elounda, Greece, June/July 1993. LNCS 697, Springer Berlin 1993, pp. 253–267.
J. C. Godskesen. Timed Modal Specifications — A Theory for Verification of Real-Time Concurrent Systems. Ph.D.Thesis, Aalborg Univ., R-94-2039, Oct. '94.
H. Hüttel and K. Larsen. The use of static constructs in a modal process logic. Proceedings of Logic at Botik'89. LNCS 363, 1989.
K.G. Larsen. Modal specifications. In: Proceedings of Workshop on Automatic Verification Methods for Finite State Systems LNCS 407, 1990.
K. Larsen and B. Thomsen. A modal process logic. In: Proceedings LICS'88, 1988.
K.G. Larsen, B. Steffen, C. Weise. A constraint oriented proof methodology based on modal transition systems. in: Proceedings 1st Workshop Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science Vol. 1019, Springer Verlag 1995, S. 17–40.
K.G. Larsen, B. Steffen, C. Weise. Fischer's Protocol Revisited: A Simple Proof Using Modal Constraints. in: Proc. Workshop on Verification and Control of Hybrid Systems, New Brunswick, 1995, to appear in LNCS.
K.G. Larsen, B. Steffen, C. Weise. A Case Study in Modal Constraint Methodology: The RPC-Memory Problem. Aachener Informatik Berichte, Technical Report, Aachen University of Technology, to appear.
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
D. Park. Concurrency and automata on infinite sequences. In P. Deussen (ed.), 5th GI Conference, LNCS 104, pp. 167–183, 1981.
L. C. Paulson. Isabelle. LNCS 828, Springer New York 1994.
B. Steffen. Generating data flow analysis from modal specifications. in: Science of Computer Programming 21, (1993), pp. 115–139.
W. Yi. CCS + Time=an Interleaving Model for Real-Time Systems, Proc.18th Int. Coll. on Automata, Languages and Programming (ICALP), Madrid, July 1991. LNCS 510, Springer New York 1991, pp. 217–228.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Larsen, K.G., Steffen, B., Weise, C. (1996). The methodology of modal constraints. In: Broy, M., Merz, S., Spies, K. (eds) Formal Systems Specification. Lecture Notes in Computer Science, vol 1169. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0024437
Download citation
DOI: https://doi.org/10.1007/BFb0024437
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61984-0
Online ISBN: 978-3-540-49573-4
eBook Packages: Springer Book Archive