CaltechTHESIS
  A Caltech Library Service

Concurrent System Design Using Flow

Citation

Hu, Cheng (2007) Concurrent System Design Using Flow. Master's thesis, California Institute of Technology. doi:10.7907/HPA7-2B52. https://resolver.caltech.edu/CaltechETD:etd-05252007-140855

Abstract

We define a formal model for concurrent systems named Flow. The goal of this formal model is to be both practical in allowing users to build the types of concurrent systems they want to build in real life and practical in allowing users to quickly prove correctness properties about the systems they build.

We define the model formally as the asynchronous product of extended state automata. Extended state automata and their asynchronous products are used to define other modeling languages as well, such as the state space exploration verification tool SPIN. Thus an offshoot of our formal definition is that we see it would not be difficult to use automated verification tools to verify Flow model properties.

Using the formal definition, we show a set of theorems that users will be able to reuse to prove correctness properties about Flow models. One category of theorems deals with showing and constructing Flow models for which all executions are guaranteed to be finite. Another category of theorems deals with showing or constructing Flow models for which all executions from a start state are guaranteed to have the same end state. This is useful because it allows users to know how all concurrent executions from a start state terminate by looking at just one execution. Another category of theorems deals with dividing complex Flow models into smaller sub-models, and showing the properties of the full model by showing the properties of the sub-models, allowing for a divide and conquer strategy to be used with Flow model proofs. The last category deals with using Hoare triples to prove properties about all executions from a set of possible start states as characterized by some pre-condition by proving properties about a set of representative executions from those start states. In the best case, we can use a combination of these techniques to show that all executions of a Flow model with start states that satisfy some pre-condition have end states that satisfy some post-condition by considering just one feasible execution of the model.

Item Type:Thesis (Master's thesis)
Subject Keywords:Concurrent system; formal modeling; formal verification
Degree Grantor:California Institute of Technology
Division:Engineering and Applied Science
Major Option:Computer Science
Thesis Availability:Public (worldwide access)
Research Advisor(s):
  • Low, Steven H.
Thesis Committee:
  • Unknown, Unknown
Defense Date:25 May 2007
Non-Caltech Author Email:1.800.chenghu (AT) gmail.com
Record Number:CaltechETD:etd-05252007-140855
Persistent URL:https://resolver.caltech.edu/CaltechETD:etd-05252007-140855
DOI:10.7907/HPA7-2B52
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:2072
Collection:CaltechTHESIS
Deposited By: Imported from ETD-db
Deposited On:05 Jun 2007
Last Modified:05 Feb 2020 20:23

Thesis Files

[img]
Preview
PDF (chenghu-masters-thesis.pdf) - Final Version
See Usage Policy.

387kB

Repository Staff Only: item control page