Integrating Object-Oriented Analysis and Formal Specifications

Formal specifications can be used to precisely describe the behavior of a computer system and its components and facilitate the development of a correct implementation using automated reasoning techniques. However, in the early stages of software development, diagrams are frequently used to describe requirements and guide development. For example, data flow diagrams (DFD) have been widely used to visualize functional behavior of processes. Entity-relationship (E-R) diagrams have been used to diagram a wide variety of concepts, foremost among them being relational data base organization. While easy to use, such notations are currently informal (hence, potentially ambiguous) and thus lack a sufficient information carrying ability necessary to capture requirements precisely. More recently, formal diagramming notations (those with a well-defined syntax and semantics) have emerged, an example being Harel's statecharts that provide a concise approach to the specification of control in a computer system.

Preliminary Investigations

Even though statecharts have been formalized, a single diagramming notation, in general, is not sufficient to capture the complex information needed to build software systems, for example, flow of control and data, component dependency, and time sequence. Accordingly, the Object Modeling Technique (OMT) uses DFDs, hybrid E-R diagrams, and statecharts to model software requirements using object-oriented concepts. The OMT notations are only partially formal (statecharts have been formalized), and methods for analysis and design with the diagrams proposed by the authors of OMT are only described informally at a high level. OMT, and its successor, UML (Unified Modeling Language) lacks the rigor needed to make its techniques amenable to formal analysis. For example, different aspects of the software requirements are represented in the three different graphical languages mentioned above, but the concepts embedded in these diagrams are interrelated. The semantics of these three graphical notations must thus be integrated in order to perform a rigorous analysis, but, currently, neither the syntax nor the semantics are rigorously defined. Nevertheless, the OMT approach, and its successor, UML, has been widely used because of its multiple views of software requirements, and it is fairly comprehensive in its (albeit informal) treatment of development issues.

This project initially involved the definition of a formal basis for an object-oriented approach to requirements acquisition, analysis, and design specification. First, we defined a precise syntax and formal semantics for the OMT diagramming notations, thus facilitating the representation and formal analysis of requirements. Using the formalized notations, an OMT model represents both a formal requirements specification and a preliminary software design, because the three complementary diagrams not only indicate what the system should achieve, but it also can be used to describe the components making up the system and their relationships. Second, we developed rigorous methods for the transformation and decomposition of OMT models that represent architectural design strategies. Third, we demonstrated how the abstract system architecture represented in the diagrams can be used to provide the foundation for a modular, formal specification of the system design. Such a specification can be used to develop an efficient executable program using either informal or formal program development methods.

This project was previously supported by a DARPA/NSF grant under the High Assurance and Evolutionary Systems programs. Click here to browse the project homepage.

Current Investigations

More recently, we have focused our investigations on UML, with an emphasis on developing embedded systems, as part of the Meridian Project. Embedded systems are typically 10 to 100 times more common than their desktop counterparts, residing in everything from engine systems, to toasters, to autopilots. The software for embedded systems is, in general, more difficult to write and debug because embedded systems software usually involves time-dependent sections in difficult to instrument situations. Embedded systems usually must achieve a higher level of robustness and reliability because they control real-world physical processes or devices upon which we depend, frequently, in a critical way. Consequently, methods for developing and modeling embedded systems and rigorously verifying behavior before committing to code, are increasingly important. Currently, much of the embedded systems industry use ad hoc approaches for developing embedded systems, where many proceed directly from requirements in prose to the target implementation language, such as C. A number of object-oriented techniques and notations have been introduced, but recently, it appears that the Unified Modeling Language (UML) could be a notation broad enough in scope to represent a variety of domains and gain widespread use. Currently, however, UML is only a notation, with no formal semantics attached to the individual diagrams or is there a formally defined semantics for the integration of the diagrams. Therefore, it is not possible to apply rigorous automated analysis to execute a UML model in order to test its behavior, short of writing code and performing exhaustive testing. We introduce a general framework for formalizing a subset of UML diagrams in terms of different formal languages based on a homomorphic mapping between metamodels describing UML and the formal language. This framework enables different modelers to target various formal languages since one formal language may be more suitable for representing the semantics of a particular domain or class of applications. This framework permits us to formulate a cocnsistent set of rules for transforming UML models to specifications in the formal alnguage. The resulting specifications derived from UML diagrams enable either simulation or analysis through model checking, using existing tools. Thus far, we have targeted two formal languages, VHDL, a language used by the embedded systems community with extensive simulation tool support, and Promela, the language used by Spin, a model checker. The framework enables us to derive VHDL specifications from the class and state diagrams in order to capture the structure and the behavior of embedded systems. The VHDL specifications enable us to perform behavior simulation of the UML models. The Promela specifications have enabled us to use Spin to perform extensive analysis of the behavior of the system as depicted by the UML diagrams.

Research Assistantships Available

A few RAships are still available for work on this project. Please contact Dr. Cheng (chengb@cse.msu.edu) for further information.

Relevant Publications and Manuscripts

  • ``Object Analysis Patterns for Embedded Systems'' S. Konrad, B.H.C. Cheng, and L. Campbell), accepted to appear in IEEE Transactions on Software Engineering.

  • ``Automated Analysis of Timing Information in UML Diagrams'' (Sascha Konrad, Laura Campbell, and Betty H.C. Cheng), In Proc. of IEEE International Conference on Automated Software Engineering, Linz, Austria, September 2004.

  • ``Automatically Detecting and Visualizing Errors in UML Diagrams,'' (with Laura A. Campbell, William E. McUmber, R.E.K. Stirewalt), Requirements Engineering Journal, Springer-Verlag, Vol. 7, No. 4, 2002, pp. 264-287.
    •
  • ``Formalizing and Integrating the Dynamic Model for Object-Oriented Modeling'' (with Enoch Y. Wang), in IEEE Transactions on Software Engineering, Vol. 28, No. 8, August 2002, pp. 747-762.
    •
  • ``Using Security Patterns to Model and Analyze Security Requirements'' (with S. Konrad, L. Campbell, and R. Wassermann), IEEE Workshop on Requirements for High Assurance Systems, (RHAS03), September 2003, Monterey, California.
    •
  • ``A Requirements Pattern-Driven Approach to Specify Systems and check Properties'' (with Sascha Konrad, Laura Campbell, and Min Deng), in IEEE SPIN 2003 Workshop, Portland, Oregon, May 2003.
    •
  • ``Requirements Patterns for Embedded Systems'' (with Sascha Konrad), IEEE Joint International Requirements Engineering Conference (RE02), September 2002, Essen Germany.
    •
  • ``Adding Formal Specifications to Requirements Patterns'' (with Sascha Konrad and Laura Campbell), IEEE Workshop on Requirements for High Assurance Systems, (RHAS02), September 2002, Essen, Germany. (Workshop affiliated with RE02).
    •
  • A General Framework for Formalizing UML (William E. McUmber and Betty H.C. Cheng), Proc. of IEEE International Conference on Software Engineering (ICSE01), May 2001, Toronto, Canada.

  • Object-Oriented Modeling and Automated Analysis of a Telemedicine Application (Laura A. Campbell and Betty H.C. Cheng), Proc. of IEEE 10th Int. Workshop on Software Specification and Design (IWSSD-10), November 2000, Shelter Island, San Diego, California.

  • "Enabling Automated Analysis through Object-Oriented Modeling Diagrams" (Betty H.C. Cheng, Laura A. Campbell, Enoch Y. Wang), in Proc. of IEEE International Conference on Dependable Systems and Networks (FTCS-30 and DCCA-8), New York, NY, June 2000.

  • ``UML-Based Analysis of Embedded Systems Using a Mapping to VHDL'' (William E. McUmber and Betty H.C. Cheng), in Proc. of IEEE High Assurance Software Engineering, Washington, DC, November 1999.

  • ``Formalizing and Integrating the Functional Model into Object-Oriented Design (Enoch Y. Wang and Betty H.C. Cheng), in Proc. of International Conference on Software Engineering and Knowledge Engineering, San Francisco, CA, June 1998.

  • ``A Rigorous Object-Oriented Design Process'' (Enoch Y. Wang and Betty H.C. Cheng), in Proc. of International Conference on Software Process, Naperville, IL, June 1998.

  • ``Formalizing and Integrating the Dynamic Model within OMT'' (Enoch Y. Wang, Heather A. Richter, and Betty H.C. Cheng), in IEEE Proc. of International Conference on Software Engineering, Boston, MA, May 1997.

  • ``A Formal Semantics of Object Models'' (Robert H. Bourdeau and Betty H.C. Cheng), in IEEE Trans. on Software Engineering, October 1995.

  • ``A Graphical Environment for Formally Developing Object-Oriented Software'' (Betty H.C. Cheng, Enoch Y. Wang and Robert H. Bourdeau), to appear in the Proc. of IEEE Int'l Conf. on Tools with Artificial Intelligence, November 1994.

  • ``Graphical Development Environment for Larch Shared and Interface Languages'' (Michele Morin and Betty H.C. Cheng), Michigan State University Technical Report, MSU-CPS-94-18 April 1994. A user manual is also available.

  • ``An Integrated Development Environment for Formal Specifications'' (with Michael R. Laux and Robert H. Bourdeau), Proc. of the IEEE 5th International Conference on Software Engineering and Knowledge Engineering, pp. 681--688, San Francisco, California, June 1993.

  • ``An Object-Oriented Toolkit for Constructing Specification Editors,'' (with Robert H. Bourdeau), Proc. 16th Annual International Computer Software and Applications Conference, 239--244, September 1992.