[cs-talks] Upcoming PhD Thesis Proposal (Thurs- Jul 14)

cs, Group cs at bu.edu
Tue Jul 12 09:22:34 EDT 2016


PhD Thesis Proposal
Combining Model Checking with Type Checking for System Verification
Zhiqiang Ren, Boston University
Thursday, July 14, 2016 at 10:30am in Hariri Center Seminar Room
Abstract:
Types have been playing a key role in many mainstream programming languages (e.g.  C/C++, Java, ML, Haskell), and type based techniques have been widely applied to software verification. On the other hand, model checking, an automated technique for systematically analyzing behaviors of systems, starts gaining its ground in software verification due to its growing popularity among developers as well as an increasing number of successful applications. In this thesis, my focus is on studying the issue of combining these two prevailing techniques synergically to support the development of designs of concurrent software systems as well as the verification of their safety and liveness properties.  In particular, I propose to design and implement a modeling language equipped with highly expressive types (including both dependent types and linear types), which is expected to greatly help detect modeling errors during the design process. I also propose to create a tool chain that not only facilitates model construction but also employs state-of-art model checking techniques in the verification of these constructed models, especially for those temporal behaviors which cannot be handled by type checking alone.

ATS is a full-fledged programming language equipped with a highly expressive type system rooted in the framework Applied Type System, which gives the language its name. In particular, both dependent types (in DML style) and linear types are available in ATS.  I propose to extend the core of ATS, which is a ML-like functional programming language into a modeling language, which inherits the type system of ATS.  The research is two pronged based on how to extend the core of ATS as well as how to use the resulting modeling language.

First, I propose to focus on one state-of-art modeling language, Promela. On one hand, I choose a subset of the syntactic core of ATS and introduce into it primitives with special operational semantics to cover features that have direct roots in Promela. Such primitives are assigned well-designed types to facilitate  a synergic combination of type checking with model checking. On the other hand, such modeling language is compiled into Promela so that the SPIN model checker can be readily used for checking models constructed in it, which gives the language its name ATS/PML. We believe that such ligtweight method would attract Promela users to start taking advantage of advanced type systems for detecting errors at compile time while constructing models targeting SPIN model checker with the consideration of verification efficiency.

Second, I propose to extend the core of ATS into an independent modeling language, in which programmers can construct models just like writing functional programs running on a virtual machine which explores all possibilities resulting from non-determinisms (e.g. scheduling).  The extension consists of various primitives, which are for modeling concurrent systems as well as specifying their properties in a programmer-centric style. Going further, these primitives are assigned well-designed types to increase the chance of constructing correct models. This modeling language is referred to as ATS/Veri, indicating its usage for software verification via both model checking and type checking. I propose to compile ATS/Veri into \csps{}, a formalism used by PAT, which is a self-contained framework to support model checking concurrent, real-time systems. Based on PAT, we can verify various properties of models in ATS/Veri including deadlock-freeness, reachability, and LTL properties with fairness assumptions.  Such work is expected to benefit the future adaption of ATS/Veri to support specification as well as verification of real-time systems via PAT.

In summary, the primary contribution of this thesis lies in the creation of a family of modeling languages with highly expressive types for modeling concurrent software systems as well as the related platform supporting the verification of various properties via model checking. As such, we can combine type checking and model checking synergically to achieve high confidence of software correctness.


Committee:
Hongwei Xi (Advisor)
Azer Bestavros
Assaf Koury

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://cs-mailman.bu.edu/pipermail/cs-talks/attachments/20160712/2f5c1464/attachment.html>


More information about the cs-talks mailing list