Loading...
Please wait, while we are loading the content...
Similar Documents
5 the Erlang Veriication Tool 3 the Speciication Language 4 the Proof System System Description: Veriication of Distributed Erlang Programs
| Content Provider | Semantic Scholar |
|---|---|
| Author | Werner, Martin Fexpr, Expr Expr: = Var J. Atom J. Pid J. Exprg Arts, Thomas Dam, Mads Fredlund, Lars-Åke Gurov, Dilian |
| Copyright Year | 1998 |
| Abstract | k rh : " (denote this proof obligation by ()), namely to proving that any process s satisfying , when put in parallel with process rh, also satisses. In fact, this is the only point at which human intervention is required. By invoking the same command, the tool explores the possible actions of s and rh, and ultimately completes the proof. If s k rh performs an input action, this can only be because of s, and if s evolves thereby to s 0 , then the resulting proof obligation becomes \s 0 : ` s 0 k rh : " which is automatically discharged against (). Similarly, if s k rh performs an output action, this can only be because of rh, and since after this action rh ceases to exist, the resulting proof obligation becomes \s : ` s : " which is an instance of the usual identity axiom of Gentzen-style proof systems. At the present point in time a rst prototype tool has been completed with the functionality described above. A number of small examples have been completed , including, as the largest, a correctness proof concerning trust of a mobile billing agent reported in DFG98]. Further information on the project and the prototype implementation can be found at http://www.sics.se/fdt/erlang/. We expect to announce a public release of the system by the end of 1998. Future work includes bigger case studies, increased support for proof automation, and better handling of fairness. The graph visualization system daVinci { a user interface for applications. assumptions s : on components s of S, are considered. Thus, the behaviour of S is speciied parametrically upon the behaviour of its components. This idea of open correctness assertions gave rise to the development of a Gentzen-style proof system DFG98] that serves as the basis for the implementation of the veriication tool. On top of a fairly standard proof system we added two rules: a \cut" rule for decomposing proofs of a system with multiple processes to proofs about the components, and a discharge rule based on detecting loops in the proof. Roughly, the goal is to identify situations where a latter proof node is an instance of an earlier one on the same proof branch, and where appropriate xed points have been safely unfolded. The discharge rule thus takes into account the history of assertions in the proof tree. In terms of … |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.ericsson.se/cslab/~thomas/cade98.ps |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
