Formal modeling and analysis of the HLA component integration standard

ABSTRACT

An increasingly important trend in the engineering of complex systems is the design of component integration standards. Such standards define rules of interaction and shared communication infrastructure that permit composition of systems out of independently-developed parts. A problem with these standards is that it is often difficult to understand exactly what they require and provide, and to analyze them in order to understand their deeper properties. In this paper we use our experience in modeling the High Level Architecture (HLA) for Distributed Simulation to show how one can capture the structured protocol inherent in an integration standard as a formal architectural model that can be analyzed to detect anomalies, race conditions, and deadlocks.

REFERENCES

• 1: Gregory D. Abowd , Robert Allen , David Garlan, Formalizing style to understand descriptions of software architecture, ACM Transactions on Software Engineering and Methodology (TOSEM), v.4 n.4, p.319-364, Oct. 1995 [doi>10.1145/226241.226244]
• 2: R. Allen. Formalism and informalism in architectural style: A case study. In Proc of the First Intl. Workshop on Architectures for Software Systems, April 1995.
• 3: Robert John Allen , David Garlan, A formal approach to software architecture, 1997
• 4: Robert Allen , David Garlan, A formal basis for architectural connection, ACM Transactions on Software Engineering and Methodology (TOSEM), v.6 n.3, p.213-249, July 1997 [doi>10.1145/258077.258078]
• 5: R. J. Allen, D. Garlan, and J. Ivers. A Wright specification of the HLA. Technical report, Carnegie Mellon University, School of Computer Science, 199s.
• 6: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 7: C. A. Damon, R. Melton, R. J. Allen, E. Bigelow, J. M. Irers, and D. Garlan. Formalizing a specification for analysis: The HLA ownership properties. Technical Report CMU-CS-93-149, Carnegie Mellon University, School of Computer Science, 1998.
• 8: Failures Divergence Refinement: FDRL User Manual. Formal Systems (Europe) Ltd., O.uford, England, version 2.22 edition, October 1997.
• 9: David Garlan , Robert Allen , John Ockerbloom, Architectural Mismatch: Why Reuse Is So Hard, IEEE Software, v.12 n.6, p.17-26, November 1995 [doi>10.1109/52.469757]
• 10: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 11: Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 12: David C. Luckham , John J. Kenney , Larry M. Augustin , James Vera , Doug Bryan , Walter Mann, Specification and Analysis of System Architecture Using Rapide, IEEE Transactions on Software Engineering, v.21 n.4, p.336-355, April 1995 [doi>10.1109/32.385971]
• 13: N. A. Lynch and M. R. Tuttle. An introduction to input/output automata. MIT/LCS/TM-373, MIT LCS, 198s. Technical Report
• 14: Jeff Magee , Naranker Dulay , Susan Eisenbach , Jeff Kramer, Specifying Distributed Software Architectures, Proceedings of the 5th European Software Engineering Conference, p.137-153, September 25-28, 1995
• 15: Mark Moriconi , Xiaolei Qian , R. A. Riemenschneider, Correct Architecture Refinement, IEEE Transactions on Software Engineering, v.21 n.4, p.356-3, April 1995 [doi>10.1109/32.385972]
• 16: James L. Peterson, Petri Nets, ACM Computing Surveys (CSUR), v.9 n.3, p.223-252, Sept. 1977 [doi>10.1145/356698.356702]
• 17: RASSP project overview, Version 1.0. CSIS TR, Dept of Electrical Engineering, University of Virginia, 1994.
• 18: A. W. Roscoe , C. A. R. Hoare , Richard Bird, The Theory and Practice of Concurrency, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 19: Mary Shaw , Robert DeLine , Daniel V. Klein , Theodore L. Ross , David M. Young , Gregory Zelesnik, Abstractions for Software Architecture and Tools to Support Them, IEEE Transactions on Software Engineering, v.21 n.4, p.314-335, April 1995 [doi>10.1109/32.385970]
• 20: D. B. Stewart, R. A. Volpe, and P. K. Khosla. Integration of real-time software modules for reconflgm-able sensor-based control systems. In Proc 1992 IEEE/RSJ Intl Conf on Intelligent Robots and Systems. IEEE Computer Society Press, July 1992.
• 21: Kevin J. Sullivan , John Socha , Mark Marchukov, Using formal methods to reason about architectural standards, Proceedings of the 19th international conference on Software engineering, p.503-513, May 17-23, 1997, Boston, Massachusetts, United States [doi>10.1145/253228.253433]
• 22: U.S. Department of Defense. High Level Architecture Interface Specification, Version 1.2, August 1997. Also available via http://www.dmso.mil/projects/hla/.
• 23: U.S. Department of Defense. High Level Architecture Interface Specification, Version 1.3, draft 1, April 1995. Also available via http://www.dmso.mil/projects/hla/.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.0 General
          Subjects: Standards

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

General Terms:
Design, Performance, Standardization, Theory

Keywords:
component integration standards, component-based software, formal specification, protocol families, software architecture