ĦĦ

Hao Ping's PhD Thesis

Object-Z/TCOZ and Timed Automata:
   Projection and IntegrationĦĦ
Thesis Draft Download
Summary

The design of complex real-time systems requires not only powerful mechanisms for modelling various aspects of a complex system but also tool support for developing the models, especially tool support for verifying the established models. While there are a variety of formal techniques and tools that have been proposed in the literature and each may has its unique strength in describing one or some aspects of a complex system, it has been realized that no single notation will ever be suitable to address all aspects of a complex system with tool support. The state-of-the-art formal modelling techniques, Z family languages OZ/TCOZ and state-machine based techniques Timed Automata, both of them have their unique strength and weakness on specifying high level abstracted models for complex systems. This thesis investigates the possible links between the modelling techniques OZ/TCOZ and TA and research how to lend the strengths of different techniques to each other or how to integrate the strengths of different techniques together so that they can be utilized coherently for building and verifying models of complex real-time systems in a unified framework. Firstly, a set of composable timed automata patterns (reminiscent of `design patterns' in object-oriented modelling) are defined based on TCOZ process constructs. These composable timed automata patterns not only provide a proficient interchange media for transforming TCOZ specifications into TA designs, which supports one possible engineering development process: TCOZ for high-level requirement specifications, then TA for design and timing analysis; but also provide a generic reusable framework for developing real-time systems in TA alone. Secondly, based on the patterns, a set of transformation rules from TCOZ to TA are defined so that one possible engineering process for modelling and checking of complex real-time system can be supported: TCOZ for building high level models and TA's tool support to be reused for verification of the models. We also investigate the semantic equivalence issue between TCOZ processes and timed automata and provide a proof for the correctness of the transformation. Lastly, inspired by this part of work, an interesting question is that: can we integrate Object-Z and Timed Automata directly? In this way, not only the wonderful tool support of TA can be reused straightforward, but also the timed composable patterns now can be directly utilized for systematic TA designs. Thus, rather than taking the transformation point of view, we also developed a novel integrated formal language which combines Object-Z with TA. The advantage of this approach lies in that by replacing TCSP with TA in TCOZ, the wonderful tool support of TA can be reused straightforward, moreover, comparing to CSP/TCSP which provide a fix topology for communications, this new formalism OZTA is injected with a novel concept of partial and sometime synchronization to capture various synchronization scenarios. Meanwhile, the OZTA notation is enhanced by introducing the set of timed patterns as language constructs to specify the dynamic and timing features of complex real-time systems in a systematic way. We also present a semantic model of OZTA in Unifying Theories of Programming which provides the semantic foundation for language understanding, reasoning and tool construction. Based on the semantic model, we constructed HighSpec an interactive system which can support editing, syntax and type checking of OZTA models as well as transforming OZTA models into TA models and Alloy Models so that we can utilize TA model-checkers, e.g., UPPAAL and Alloy Analyzer, for verification and analysis.
In summary, we built up the linkages of different modelling techniques, Object-Z/TCOZ and Timed Automata, and established a powerful unified framework using two alternative approaches for modelling and checking of complex real-time systems.
ĦĦ

Thesis Structure

  • Chapter 1: Introduction
    • Motivation and Goals
    • Outline of This Thesis
    • Publications from the Thesis
  • Chapter 2: OZ/TCOZ and Timed Automata
    • Object-Z
    • Timed Communicating Sequential Process

    • Timed Communicating Object-Z

    • Timed Automata

  • Chapter 3: Composable TA patterns

    • Z definition of Timed Automata

    • TA patterns

    • Generating New Patterns

    • Guidelines for TA Design Using Patterns

    • Discussion and Conclusion

  • Chapter 4: Projection from TCOZ to TA

    • Introduction

    • Mapping Rules

    • Correctness

    • An Example: Railroad Crossing System

    • Tool Support

    • Conclusion

  • Chapter 5: Case Study: Multi-terminal Railcar System

    • TCOZ Model of MRS

    • Translation

    • Model-checking MRS

    • Conclusion

  • Chapter 6: Integrating Object-Z with Timed Automata
    • Introduction

    • Overview on Combining Object-Z and TA

    • Design Decision

    • Composition and Communication

    • Operational Semantics

    • An Example: Electronic Key System

  • Chapter 7: OZTA Semantics
    • Introduction

    • The Syntax of OZTA

    • The Semantics of OZTA

    • Conclusion

  • Chapter 8: OZTA Tool Support and Case Study

    • Introduction

    • Modeling

    • Checking

    • Case Study: A Frog Puzzle Game

    • Conclusion
  • Chapter 9: Conclusion
    • Conclusion
    • Future Work
  • Appendix

Selected Publications and Submission from the Thesis

  • J. S. Dong, P. Hao, X. Zhang, and S. Qin, HighSpec: a Tool for Building and Checking OZTA Models. 28th International Conference on Software Engineering (ICSE06). Research Demonstration. ACM Press, pp 775-778, Shanghai, China. 2006
  • J.S. Dong and P. Hao and B. Mahony, Formal Designs for Embedded and Hybrid Systems. International Journal on Software Engineering and Knowledge Engineering, vol 15(2): 373-378, 2005
  • J. S. Dong, P. Hao, X. Zhang, and S. Qin, OZTA Semantics and Tool support, The 7th International Conference on Formal Engineering Methods (ICFEM'05), Manchester, UK, 2005 Nov
  • J. S. Dong, R. Duke and P. Hao, Integrating Object-Z with Timed Automata, The 10th IEEE International Conference on Engineering of Complex Computer System, Shanghai, 2005 June.
  • J. S. Dong, P. Hao, S. Qin, J. Sun and Y. Wang. Timed Patterns: TCOZ to Timed Automata, The 6th International Conference on Formal Engineering Methods (ICFEM'04), Seattle, USA, Nov. 2004.Ħħ

  • J. S. Dong, P. Hao, S. Qin, J. Sun and Y. Wang, Timed Composable Patterns: From TCOZ to Timed Automata, submitted to ACM Transactions on Software Engineering and Methodology for the second round review.

Last updated: 01/16/2007