Modeling SPARK systems with UML

ABSTRACT

In this paper, we will consider two aspects of UML in order to assess how well suited it is for modeling SPARK systems. The first aspect is the ability to represent SPARK in UML from a theoretical perspective. The second aspect is more from a hands-on perspective and evaluates what makes a UML CASE-tool more suitable for modeling SPARK systems than another.

REFERENCES

• 1: John Barnes , J. G. Barnes, High Integrity Software: The SPARK Approach to Safety and Security, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2003
• 2: OMG, Unified Modeling Language Specification, Version 1.5, OMG Document formal /2003-03-01
• 3: Amey, P., Correctness by Construction: Better Can Also Be Cheaper, CrossTalk Journal, March 2002.
• 4: ECMA TR/55 Reference Model For Frameworks Of Software Engineering Environments. 3rd Edition, June 1993
• 5: Amey, P, The INFORMED Design Method for SPARK. Praxis Critical Systems 1999, 2003.
• 6: Amey, P., White, N., High-Integrity Ada in a UML and C World. Lecture Notes in Computer Science 3063. A Llamosi and A.Strohmeier (Eds.): Reliable Software Technologies - Ada-Europe 2004 9th Ada-Europe International Conference, Palma de Mallorca, Spain, June 2004, 225--236

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Computer-aided software engineering (CASE)

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Object-oriented languages; Data-flow languages

General Terms:
Design, Languages

Keywords:
SPARK, UML, ada, informed, metamodel, profile