Abstract
A specification of a software system involves several aspects. Two essential aspects are convenience in specification and possibility for formal analysis. These aspects are, to some extent, exclusive. This paper describes an approach to the specification of systems that emphasizes both aspects, by combining UML with a language for description of the observable behavior of object viewpoints, OUN. Whereas both languages are centered around object-oriented concepts, they are complementary in the sense that one is graphical and semi-formal while the other is textual and formal. The approach is demonstrated by a case study focusing on the specification of an open communication infrastructure.
This work is financed by the Research Council of Norway under the research program for Distributed IT-Systems.
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
G. A. Agha, I. A. Mason, S. F. Smith, and C. L. Talcott. A foundation for actor computation. Journal of Functional Programming, 7(1):1–72, Jan. 1997.
T. Akerbaek and M. Louka. The software bus, an object-oriented data exchange system. Technical Report HWR-446, OECD Halden Reactor Project, Institute for Energy Technology, Norway, Apr. 1996.
D. B. Aredo, I. Traore, and K. Stlen. Towards a formalization of UML class structure in PVS. Research Report 272, Dept. of Informatics, Univ. of Oslo, 1999.
T. Bolognesi and E. Brinksma. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, 14(1):25–59, 1987.
G. Booch. Object-Oriented Analysis and Design with Applications. Benjamin-Cummings, Redwood City, CA, 1991.
G. Booch, J. Rumbaugh, and I. Jacobson. The Unified Modeling Language User Guide. Addison-Wesley, Reading, Massachusetts, USA, 1999.
J. Eiler. Critical safety function monitoring: an example of information integration. In Proceedings of the Specialists’ Meeting on Integrated Information Presentation in Control Rooms and Technical Offices at Nuclear Power Plants (IAEA-I2-SP-384.38), pages 123–133, Stockholm, Sweden, May 2000.
C. A. R. Hoare. Communicating Sequential Processes. International Series in Computer Science. Prentice Hall, Englewood Cliffs, NJ, 1985.
ITU Recommendation X.901-904 ISO/IEC 10746. Open Distributed Processing-Reference Model parts 1-4. ISO/IEC, July 1995.
I. Jacobson, M. Christerson, P. Jonsson, and G. Övergaard. Object-Oriented Software Engineering: A Use Case Driven Approach. Addison-Wesley, 1992.
E. B. Johnsen and O. Owe. A PVS proof environment for OUN. Research Report 295, Department of informatics, University of Oslo, 2001.
E. B. Johnsen and O. Owe. A compositional formalism for object viewpoints. In Proc. 5th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2002). Kluwer Academic, 2002. To appear.
E. B. Johnsen, O. Owe, E. Munthe-Kaas, and J. Vain. Incremental fault-tolerant design in an object-oriented setting. In Proceedings of the Asian Pacific Conference on Quality Software (APAQS’01). IEEE press, Dec. 2001.
G. Kahn. The semantics of a simple language for parallel programming. In J. L. Rosenfeld, editor, Information Processing 74: Proceedings of the IFIP Congress 74, pages 471–475. IFIP, North-Holland Publishing Co., Aug. 1974.
A. Kleppe and J. Warmer. Extending OCL to include actions. In A. Evans, S. Kent, and B. Selic, editors, Proceedings of UML 2000, volume 1939 of Lecture Notes in Computer Science, pages 440–450, York, UK, Oct. 2000. Springer-Verlag.
F. Kostiha. Establishment of an on-site infrastructure to facilitate integration of software applications at Dukovany NPP. In Proceedings of the Specialists’ Meeting on Integrated Information Presentation in Control Rooms and Technical Offices at Nuclear Power Plants (IAEA-I2-SP-384.38), Stockholm, Sweden, May 2000.
L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.
J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96:73–155, 1992.
R. Milner. Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, May 1999.
Object Management Group. UML Language Specification, version 1.4, Sept. 2001.
O. Owe and I. Ryl. OUN: a formalism for open, object oriented, distributed systems. Research Report 270, Dept. of informatics, Univ. of Oslo, Aug. 1999.
S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for faulttolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, Feb. 1995.
D. L. Parnas and Y. Wang. The trace assertion method of module interface specification. Technical Report 89-261, Department of Computing and Information Science, Queen’s University at Kingston, Kingston, Ontario, Canada, Oct. 1989.
J. Rumbaugh, M. Blaha, W. Premerlani, F. Eddy, and W. Lorensen. Object-oriented Modeling and Design. Prentice Hall, Englewood Cliffs, New Jersey, 1991.
G. Smith. The Object-Z Specification Language. Advances in Formal Methods. Kluwer Academic Publishers, 2000.
I. Traore, D. B. Aredo, and K. Stlen. Formal development of open distributed systems: Towards an integrated framework. In Proc. Workshop on Object-Oriented Specification Techniques for Distributed Systems and Behaviours (OOSDS’99), Paris, France, Sept. 1999.
J. Warmer and A. Kleppe. The Object Constraint Language: Precise Modeling with UML. Object Technology Series. Addison-Wesley, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Johnsen, E.B., Zhang, W., Owe, O., Aredo, D.B. (2002). Combining Graphical and Formal Development of Open Distributed Systems. In: Butler, M., Petre, L., Sere, K. (eds) Integrated Formal Methods. IFM 2002. Lecture Notes in Computer Science, vol 2335. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47884-1_18
Download citation
DOI: https://doi.org/10.1007/3-540-47884-1_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43703-1
Online ISBN: 978-3-540-47884-3
eBook Packages: Springer Book Archive