Complementary formalisms - synthesis, verification and visualization

Over the last few decades, many specification languages have been proposed. Two complementary approaches have proven useful in practice. Logic-based formalisms are based on mathematical techniques which provide the means for defining consistency, completeness, refinement, etc. Diagrammatic formalisms 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. An important part of this thesis is dedicated to the synthesis problem. For system engineering starting with logic-based models, we developed a method of synthesizing finite state machines from Object-Z models with history invariants. For system development starting with diagrams, we investigated ways of synthesizing distributed object systems from Live Sequence Charts. By combining the two approaches, we achieve the goal of generating implementations from complicated system specifications. This thesis also investigates sound transformations between different formalisms for visualization and verification.

Author dc:creator

• SUN JUN

• Synthesis, Verification, Visualization, Z/Object-Z, CSP/Timed CSP, MSC/LSC