Hu, Cheng (2007) Concurrent system design using Flow. Master's thesis, California Institute of Technology. http://resolver.caltech.edu/CaltechETD:etd-05252007-140855
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)|
|Defense Date:||25 May 2007|
|Non-Caltech Author Email:||1.800.chenghu (AT) gmail.com|
|Default Usage Policy:||No commercial reproduction, distribution, display or performance rights in this work are provided.|
|Deposited By:||Imported from ETD-db|
|Deposited On:||05 Jun 2007|
|Last Modified:||26 Dec 2012 02:46|
- Final Version
See Usage Policy.
Repository Staff Only: item control page