กก

Jun Sun's PhD Thesis
Title: Complementary Formalisms - Synthesis, Verification and Visualization
Thesis Draft Download
  • For Review Version (1.5 lined,11pt): PDF.
Abstract

Over the last few decades, many specification languages have been proposed, targeting different systems, different aspects of complex systems, and systems at different stages of development. Two complementary approaches have proven useful in practice. Logic-based formalisms like Z and CSP are based on mathematical techniques which provide the means for defining notions like consistency, completeness, and correctness. Chart-based formalisms like sequence charts or Statecharts are based on visual transition diagrams and are widely accepted by industry. One challenge of designing complex computer systems is to find benefiting formalisms from those that may vary significantly in presentation and establish sound connections between them. A long-cherished goal of software engineering is the mechanized synthesis of implementations from high-level specifications. An important part of this thesis is dedicated to the problem of synthesis. For system engineering starting with state-based formal specification, we developed a method of synthesizing implementable finite state machines from logic-based Object-Z models with history invariants. For system development starting with scenario-based specification, we investigated ways of synthesizing distributed object systems from Live Sequence Charts without constructing the global state machine. By combining the two approaches, we achieve the goal of generating implementations from system specifications with not only complicated control flow but also complex data structures. In addition tothe p roblem of synthesis, this thesis also investigates the sound transformation between different formalisms so that existing theory and tool support can be reused for objectives including visualization and verification. Logic-based models can be visualized by diagrammatic languages like UML to allow easy grasp of essential facts. Using transformation techniques, mature verification mechanisms can be reused over formalisms other than those intended to discover design errors inexpensively. In a nutshell, we established various connections between reciprocal' logic-based and chart-based formalisms, which provide constructive methods for system development.
กก
Funding

This project receives funding and rewards from the following:

  • "Rigorous Design Methods and Tools for Intelligent Autonomous Multi-Agent Systems" supported by Ministry of Education (MOE) of Singapore.

  • "Defense Innovative Research Project (DIRP) - Formal Methods and DAML" supported by Defense & Science Technology Agency (DSTA) of Singapore.

  • "Reliable Software Design and Development for Sensor Network Systems" supported by National University of Singapore Academic Research Fund.

  • Dean's Graduate Award, 2005, School of Computing, National University of Singapore.

Thesis Structure
  • Chapter 1: Introduction and Overview
    • Motivation and Goals
    • Thesis Outline and Overview
    • Publications from the Thesis
  • Chapter 2: Notations and Languages
    • State-based Formalisms
    • Event-based Formalisms
  • Chapter 3: Visualization
    • Introduction
    • An Integrated Specification Language
    • From TCOZ to Statecharts
    • From TCOZ to Scenarios
    • Summary
  • Chapter 4: Verification
    • Model Checking Live Sequence Charts
    • Verification of Timed CSP and TCOZ
    • Summary
  • Chapter 5: Synthesis from Scenario-based Specification
    • Introduction
    • CSP with Liveness
    • Refined CSP modeling of LSC
    • Synthesis
    • Generating Implementations
    • Summary
  • Chapter 6: Synthesis from State-based Specification
    • Introduction
    • Extracting Raw State Machine
    • Refining the Finite State Machine
    • Discussion
    • Summary
  • Chapter 7: From Scenarios with Data to Implementations
    • Introduction
    • Integrating Live Sequence Chart and Z
    • Synthesis of Distributed Object System
    • Refinement of the Distributed Object System
    • Automation
    • Summary and Discussion
  • Chapter 8: Conclusion
    • Conclusion
    • Future Research Trends
  • Appendix

Selected Publications from the Thesis

Last updated: 11/28/2006