Abstract
Concurrent systems are intricate and difficult to reason about. Development of ‘good’ systems require tool supported notations where formal specifications can be related to executable code. This paper presents an example of how the RAISE Specification Language, RSL, can be utilised to abstract the safety properties from a sequential imperative program communicating values, so that they can be supplemented by progress requirements and environment assumptions. In this way a process algebra approach is linked to temporal reasoning within the same language. Developments and system properties are justified by means of the RAISE tools' justification editor. General schemes for specifying safety and progress properties of deterministic state transition systems are provided.
This report reflects work which is partially funded by the Commission of the European Communities (CEC) under the ESPRIT II programme in the area of Information Processing Systems, project no. 5383: “Large-scale Correct Systems Using Formal Methods”.
Preview
Unable to display preview. Download preview PDF.
References
The RAISE Language Group: The RAISE Specification Language, Prentice Hall (1992)
The RAISE Method Group: The RAISE Development Method, Prentice Hall (to appear)
P.M. Bruun et. al: RAISE Tools Reference Manual, LACOS/CRI/DOC/13/0/V2 (1993)
D. Bolignano, M. Debabi: Higher order communicating processes with valuepassing, assignment and return of results, Proceedings of the ISAAC'92 Conference, LNCS 650. Springer Verlag (1992)
C. George, R. Milne: Specifying and refining concurrent systems. In: C. Morgan, J.C.P. Woodcock (eds): 3rd Refinement Workshop, Springer Verlag (1990)
C.A.R. Hoare: Communicating Sequential Processes, Prentice Hall (1985)
R. Milner: Communication and Concurrency, Prentice Hall (1989)
A. U. Shankar: An introduction to Assertional Reasoning for Concurrent Systems, ACM Clomp. Surveys Vol. 25 No. 3 (Sep. 1993)
M. Abadi, L. Lamport: Composing Specifications, ACM TOPLAS Vol.15 No.1 (Jan 1993)
S. S. Lam, A. U. Shankar: A Theory of Interfaces and Modules — I: Composition Theorem, IEEE Transactions on Software Engineering Vol. 20 No. 1 (Jan 1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gørtz, J. (1994). Specifying safety and progress properties with RSL. In: Naftalin, M., Denvir, T., Bertran, M. (eds) FME '94: Industrial Benefit of Formal Methods. FME 1994. Lecture Notes in Computer Science, vol 873. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58555-9_116
Download citation
DOI: https://doi.org/10.1007/3-540-58555-9_116
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58555-8
Online ISBN: 978-3-540-49031-9
eBook Packages: Springer Book Archive