Abstract
A model is a simplified representation of the real world and, as such, includes only those aspects of the real-world system relevant to the problem at hand. The paper reviews a modelling approach to the design of concurrent programs in which models represent the behaviour of concurrent Java programs. A notation based on CSP is used to model behaviour. Tool support enables both interactive model exploration and the mechanical verification of required safety and liveness properties. Models are systematically translated into Java programs. The approach, supported by a textbook, forms the basis of a course at the authors’ institution and has also been widely adopted elsewhere. With the benefit of five years hindsight, we examine the strengths and weaknesses of the approach and look at some of the subsequent remedies and directions.
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.
References
Magee, J., Kramer, J.: Concurrency: State Models & Java Programs. John Wiley & Sons, Chichester (1999)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)
Cheung, S.C., Kramer, J.: Checking Safety Properties Using Compositional Reachability Analysis. ACM Transactions on Software Engineering and Methodology 8(1), 49–78 (1999)
Giannakopoulou, D., Magee, J., Kramer, J.: Checking Progress with Action Priority: Is it Fair? In: Nierstrasz, O., Lemoine, M. (eds.) ESEC 1999 and ESEC-FSE 1999. LNCS, vol. 1687, pp. 511–527. Springer, Heidelberg (1999)
Giannakopoulou, D., Magee, J.: Fluent Model Checking for Event-Based Systems. In: Proc. of the 4th joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2003), Helsinki (2003)
Chatley, R., Eisenbach, S., Kramer, J., Magee, J., Uchitel, S.: Predictable Dynamic Plugin Systems. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol. 2984, pp. 129–143. Springer, Heidelberg (2004)
Uchitel, S., Kramer, J., Magee, J.: Incremental Elaboration of Scenario-Based Specifications and Behaviour Models using Implied Scenarios. In: Transactions on Software Engineering and Methodology (TOSEM), vol. 13(1), pp. 37–85. Association of Computing Machinery Press
Magee, J., Kramer, J., Giannakopoulou, D., Pryce, N.: Graphical Animation of Behavior Models. In: Proc. of the 22nd International Conference on Software Engineering (ICSE 2000), Limerick, June 2000, pp. 499–508 (2000)
Foster, H., Kramer, J., Magee, J., Uchitel, S.: Model-based Verification of Web Service Compositions. In: Proc. of the Automated Software Engineering, Montreal, IEEE CS Press, Los Alamitos
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Magee, J., Kramer, J. (2005). Model-Based Design of Concurrent Programs. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds) Communicating Sequential Processes. The First 25 Years. Lecture Notes in Computer Science, vol 3525. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11423348_11
Download citation
DOI: https://doi.org/10.1007/11423348_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25813-1
Online ISBN: 978-3-540-32265-8
eBook Packages: Computer ScienceComputer Science (R0)