S.-K. Kim, Dept. of Comput. Sci. & Electr. Eng., Queensland Univ., Brisbane, Qld., Australia
D. Carrington, Dept. of Comput. Sci. & Electr. Eng., Queensland Univ., Brisbane, Qld., Australia
Presents a framework that integrates a graphical specification technique (UML) with a formal specification technique (Object-Z) to support requirements elicitation and analysis activities. Various UML diagrams are used to specify the system from different concerns during the early requirements elicitation and analysis stage. The information captured in the diagrams is used to develop a complete Object-Z specification. This paper presents a semantic translation from statechart diagrams to Object-Z specifications. Finally, based on information captured in sequence diagrams and use case diagrams, a functional model of the whole system is formally defined. The case study used in this paper is a real-time, interactive and embedded system: a light control system.
Index Terms:
formal specification; specification languages; diagrams; lighting control; object-oriented languages; object-oriented methods; Unified Modeling Language; Object-Z specifications; integrated framework; precise understandable specification; light control system; case study; graphical specification technique; formal specification technique; requirements elicitation; systems analysis; UML diagrams; semantic translation; statechart diagrams; sequence diagrams; use case diagrams; functional model; real-time interactive embedded system
Citation:
S.-K. Kim, D. Carrington, "An integrated framework with UML and Object-Z for developing a precise and understandable specification: the light control case study," apsec, pp.240, Seventh Asia-Pacific Software Engineering Conference (APSEC'00), 2000
PURCHASE ARTICLE: $19
IEEE Xplore Subscribers
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb