Thumbnail
Access Restriction
Open

Author Rajamani, Sriram K. ♦ Rehof, Jakob
Source CiteSeerX
Content type Text
Publisher Springer-Verlag
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword State Explosion ♦ Deadlock Freedom ♦ Sequential Programming Language ♦ Type System ♦ Assume-guarantee Reasoning ♦ Assume-guarantee Rule ♦ Promising Approach ♦ Behavioral Type System ♦ Circular Assume-guarantee Reasoning Principle ♦ Behavioral Type System Work ♦ Type Checking Problem ♦ Model Checking ♦ Appropriate Concurrent Context ♦ Type Inference ♦ Behavioral Specification ♦ Exponential Cost ♦ Pi-calculus Program ♦ Many Interesting Program Property ♦ Behavioral Module System ♦ Realistic Concurrent Program ♦ Asynchronous System ♦ Communication Progress ♦ Module System ♦ Behavioral Property ♦ Fundamental Principle ♦ Fundamental Challenge
Description Distributed message-passing based asynchronous systems are becoming increasingly important. Such systems are notoriously hard to design and test. A promising approach to help programmers design such programs is to provide a behavioral type system that checks for behavioral properties such as deadlock freedom using a combination of type inference and model checking. The fundamental challenge in making a behavioral type system work for realistic concurrent programs is state explosion. This paper develops the theory to design a behavioral module system that permits decomposing the type checking problem, saving exponential cost in the analysis. Unlike module systems for sequential programming languages, a behavioral specification for a module typically assumes that the module operates in an appropriate concurrent context. We identify assume-guarantee reasoning as a fundamental principle in designing such a module system. Concretely, we propose a behavioral module system for pi-calculus programs. Types are CCS processes that correctly approximate the behavior of programs, and by applying model checking techniques to process types one can check many interesting program properties, including deadlockfreedom and communication progress. We show that modularity can be achieved in our type system by applying circular assume-guarantee reasoning principles whose soundness requires an induction over time. We state and prove an assume-guarantee rule for CCS. Our module system integrates this assume-guarantee rule into our behavioral type system.
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article
Publisher Date 2001-01-01
Publisher Institution In Proc. of Static Analysis Symposium (SAS