Complementary formalisms - synthesis, verification and visualization
type: CreativeWork
description: 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.
abstract: 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: SUN JUN
keywords: Synthesis, Verification, Visualization, Z/Object-Z, CSP/Timed CSP, MSC/LSC
date published: 2006-09-28
date modified: 2026-07-24T03:32:30Z
provider: National University of Singapore
publisher: Networked Digital Library of Theses and Dissertations
type: WebPage
source organization: National University of Singapore