HCES 2003 @ Carnegie Mellon

Bogor: An Extensible and Highly-Modular Software Model-Checking Framework

We believe that with appropriate tool support, domain experts will be able to develop efficient model checking-based analyses for a variety of software-related models. To explore this hypothesis, we have developed Bogor, a model checking framework with an extensible input language for defining domain-specific constructs and a modular interface design to ease the optimization of domain-specific state-space encodings, reductions and search algorithms. We present the pattern-oriented design of Bogor and discuss our experiences adapting it to efficiently model check Java programs and event-driven component-based designs.

Carnegie Mellon	Specification and Verification Center
Kansas State University	Laboratory for Specification, Analysis and Transformation of Software
University of Pennsylvania	Real-Time Systems Group

David Arney University of Pennsylvania	Translating Informal Requirements to Formal Models: Two Case Studies The poster presents two projects in which natural language informal requirements are translated into sets of extended finite state machines. The systems considered are a control algorithm for a medical device and the regulations governing the testing of blood donations for Hepatitis B. We examine merging multiple sets of requirements, ways in which some operations might be automated, and using the resulting model for property checking and simulation.

Sagar Chaki Carnegie Mellon University	Model checking embedded software written in C We present research aimed at verifying concurrent C programs. Our approach is completely automated and is based on the counterexample guided abstraction refinement paradigm. State space explosion is handled via abstraction techniques like predicate abstraction. Further, attempt is made to minimize the number of predicates involved in the abstraction process. We have been able to handle industrial size examples, including a metal casting controller system comprised of 30,000 lines of C.

Ed Clarke and Joel Ouaknine (The co-authors of the work are Ed Clarke, Daniel Kroening, Joel Ouaknine, and Ofer Strichman.) Carnegie Mellon University	Completeness of Bounded Model Checking: From Finding Bugs to Proving Correctness Brief Abstract: Bounded Model Checking is a technique for finding bugs of fixed depth in, e.g., chip designs, embedded controllers, communication protocols, etc. However, in order to prove systems correct (vital for high-confidence embedded systems), a pre-computed "completeness threshold" must be known. Our research has focussed on efficient techniques to tightly over-approximate this completeness threshold for arbitrary models and specifications.

Bob Cook Georgia Southern University	The Linux Kernel Verification Project (LV) The LV project has the goal of adding value to the world-wide Linux Open Source initiative by using state-of-the-art verification tools, most notably SPIN, to improve the operating systems’ code base. The methodology is to select kernel modules, to translate the code to a verification specification, to analyze the code, and then to post bugs and fixes back to the international Linux repository. Aside from the anticipated benefits to Linux, the project will also document deficiencies in verification languages and implementations. The models will also be posted on the web as test problems for other verification tools. The presentation will use the setuid system call as an example.

Matt Dwyer and John Hatcliff Kansas State University	Cadena: An Integrated Development, Analysis, and Verification Environment for Component-based Systems We present Cadena -- an integrated environment for building and modeling CORBA Component Model (CCM) systems. Cadena provides facilities for defining component types using CCM IDL, specifying dependency information and transition system semantics for these types, assembling systems from CCM components, visualizing various dependence relationships between components, specifying and verifying correctness properties of models of CCM systems derived from CCM IDL, component assembly information, and Cadena specifications, and producing CORBA stubs and skeletons implemented in Java. We are applying Cadena to avionics applications built using Boeing's Bold Stroke framework.

Ansgar Fehnker Carnegie Mellon University	The Verification Toolbox The Verification Toolbox (VTB) is a new tool for analyzing and managing model based designs of embedded systems through simulation and formal verification. The toolbox is realized in MATLAB to support model-based design in the Simulink/ StateFlow environment.

Ansgar Fehnker and Michael Theobald (joint work with Edmund Clarke, Zhi Han, Bruce Krogh, Joel Ouaknine, and Olaf Stursberg) Carnegie Mellon University	Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems With the increasing use of hybrid systems to design embedded controllers for complex systems such as manufacturing processes, automobiles, and transportation networks, there is an urgent need for more powerful analysis tools, especially for safety critical applications. Properties of hybrid systems, which have an infinite state space, can often be verified using ordinary model checking together with a finite-state abstraction. Model checking can be refined. We present a new procedure to perform this refinement operation for abstractions of hybrid systems, using the counterexample generated by the model checker. Experimental results for a prototype implementation indicate significant advantages over existing methods.

David Garlan, Bradley Schmerl Carnegie Mellon University	Architecture-Based Dynamic Adaptation Software architectures provide an abstract model of a software system that can be used as the basis for formal analysis of that system. In the Rainbow project, we provide infrastructure that makes architecture and architecture analysis available at runtime, to monitor and guide the dynamic adaptation of executing systems. Using that architecture as the basis for dynamic repair provides understandable, analyzable, and adaptable change policies that ease the software engineering of software that needs to respond to changes in its environment.

David Garlan, Bradley Schmerl Carnegie Mellon University	Formal Verification of Software Architectures Software architectures provide an abstract model of a software system that can be used as the basis for formal analysis of that system. Providing tool support for developing software architectures, checking architectural constraints and conformance to architectural style, is crucial in making software architectures accessible to software engineers. We demonstrate such a tool, called AcmeStudio, and show how it is being applied to NASA’s Mission Data System, a framework that has a complex architectural style.

Alwyn Goodloe University of Pennsylvania	OpEm: Open APIs for Embedded Systems The OpEm project at Penn is concerned with technologies that address the barriers to embedded computer systems that provide open APIs so they can be programmed by parties other then the platform vendor. OpEm focuses on techniques from formal methods and programming languages to address these concerns. Our current effort is in the area of programmable for "programmable payment cards" that support policy refinements by parties different from the one that issued the card. A sample application is an enterprise that would like to create custom cards for its employees without the direct involvement of the card issuer (typically a bank).

Alex Groce Carnegie Mellon University	Model checking provides the ability to find errors in systems However, currently, the process of localizing and fixing the errors is essentially automated. Error explanation uses a model checker to aid users in finding the true causes of bugs and suggests fixes to code.

Elsa L. Gunter New Jersey Institute of Technology	Requirements Management System As product is developed from preliminary design through testing and revision, it is desirable/necessary to be able trace the connection of system specifications, code, test suites, and verification formalisms back to the evolving requirements. We describe the design of a tool to facilitate the management of requirements, including the ability to record for each requirements statement attributes such as which components it relates to and which formal specifications guarentee it. The requirements document constructed with this tool can then be querried and a flitered view created allowing users to gather together all parts that relate to a given topic, have a given attribute, or relate to a particular formal specifcation.

Zhi Han and Bruce Krogh Carnegie Mellon University	Model Reduction for Verification of Hybrid Systems Verification of hybrid systems has been studied for embedded control systems to provide guaranteed properties. Existing tools can only verify systems with limited number of continuous variables. Model reduction is a technique to approximate the behavior of a complex system with reduced number of continuous variables. This presentation summarizes our recent effort to apply model reduction to verification problems.

Franjo Ivancic University of Pennsylvania	Counter-Example Guided Predicate Abstraction of Hybrid Systems An embedded system typically consists of a collection of digital programs that interact with each other and with an analog environment. An embedded system consisting of sensors, actuators, plant, and control software is best viewed as a hybrid (mixed discrete-continuous) system. This talk presents the concept of counter-example guided predicate abstraction for invariant verification of hybrid systems using polyhedral approximations.

Jim Kapinski Carnegie Mellon University	Systematic Simulation for Exploring Embedded Control System Design Current techniques for verification of designs of embedded controllers for continuous and hybrid dynamic systems are computationally expensive. This poster presents a new technique for exploring the continuous-state behaviors of embedded control systems based on finite-state machine techniques. Connectivity between sets of reachable states is represented by transitions in an FSM with labels corresponding to values of the system input. The key idea is to reduce the number of states in the FSM representation by merging reachable sets that are close together. In some cases the breadth-first exploration of the reachable state space terminates, meaning that the FSM represents the reachable states for unbounded time. Results are presented for a servo system example.

Jesung Kim University of Pennsylvania	Model-based Code Generation for Hybrid Systems Benefits of high-level modeling and analysis are significantly enhanced if code can be generated automatically from a model such that the correspondence between the model and the code is precisely understood. For embedded control software, hybrid systems is an appropriate modeling paradigm because it can be used to specify continuous dynamics as well as discrete switching between modes. In this research, we propose an approach to compile the modeling language CHARON that allows hierarchical specifications of interacting hybrid systems. The approach is illustrated by compiling a model for coordinated motion of legs for walking onto Sony's AIBO robot.

Daniel Kroening Carnegie Mellon University	Bridging the Gap between Legacy Code and Formal Specification Most embedded systems are legacy designs, i.e., written in a low level language such as ANSI-C or even assembly language, or at least contain components that are written in this manner. Very often performance requirements enforce the use of these languages. These systems are a bigger problem than the new, high-level designs, but the existing tools do not address the verification problem. We present technology that allows the verification of such legacy code with respect to a formal specification.

Bruce Krogh Carnegie Mellon University	VTB Model Relations Manager The "Model Relations Manager" is a component of the Verification Toolbox. The MRM focuses on consistently managing the models themselves and their evolution. Models are decomposed into submodels and exist in multiple variants. It also supports consistency checking of different model configurations by constraining the variant selection and change impact analysis and propagation by identifying submodels within a model, across model configurations, as well as previously validated requirements that can be and have been affected by model changes.

Flavio Lerda, Edmund Clarke Carnegie Mellon University	MicroC/OS: A Case Study of the Verification of a Real-Time Operating System Many embedded systems contain a real-time operating system. The operating system is at that the heart of the system as it offers the basic functionalities that are used by the applications. The correctness of the operating system is therefore crucial to the correctness of the embedded system itself. MicroC/OS is a real-time operating system that has been used in many real world embedded systems. We present preliminary work in using MicroC/OS as a case study in the verification of a real-time operating system. One of main aspects that we have looked at so far is the specification of the properties we want to prove: we identified two kinds of properties, one related to the timing constraints that the system has to satisfy, and one related to the correctness of the functionalities offered by the operating system. We made progress on both sides and we are currently implementing prototype tools with which we are planning to prove properties of MicroC/OS.

P. Madhusudan, Wonhong Nam and Rajeev Alur. University of Pennsylvania	Symbolic Computational Techniques for Solving Games Games are useful in modular specification and analysis of systems where the distinction among the choices controlled by different components is made explicit. In this poster, we formulate and compare various symbolic computational techniques for deciding existence of winning strategies. The first technique employs symbolic fixpoint computation using BDDs and the second technique checks for the existence of strategies that ensure winning within k steps by reduction to the satisfiability of quantified boolean formulas. We compare the various approaches on two examples using existing tools such as Mucke, Mocha, Quaffle, Qube, BerkMin and zChaff.

Joel Ouaknine (Joint work with Ed Clarke, Daniel Kroening, and Ofer Strichman) Carnegie Mellon University	The completeness threshold for bounded model checking The LV project has the goal of adding value to the world-wide Linux Open Source initiative by using state-of-the-art verification tools, most notably SPIN, to improve the operating systems’ code base. The methodology is to select kernel modules, to translate the code to a verification specification, to analyze the code, and then to post bugs and fixes back to the international Linux repository. Aside from the anticipated benefits to Linux, the project will also document deficiencies in verification languages and implementations. The models will also be posted on the web as test problems for other verification tools. The presentation will use the setuid system call as an example.

Robby Kansas State University	Bogor: An Extensible and Highly-Modular Software Model-Checking Framework We believe that with appropriate tool support, domain experts will be able to develop efficient model checking-based analyses for a variety of software-related models. To explore this hypothesis, we have developed Bogor, a model checking framework with an extensible input language for defining domain-specific constructs and a modular interface design to ease the optimization of domain-specific state-space encodings, reductions and search algorithms. We present the pattern-oriented design of Bogor and discuss our experiences adapting it to efficiently model check Java programs and event-driven component-based designs.

Usa Sammapun University of Pennsylvania	Run-time Monitoring, Checking and Steering The run-time monitoring, checking and Steering (MaCS) provide assurance that a target program is running correctly with respect to formal requirements specification. MaCS bridges the gap between formal verification and testing. The monitor and checking components dectect propery violation whereas the steering component provide feedback and steer the application back to a safe state after an error occurs. We present a case study where MaCS is used in a control system that keeps an inverted pendulum upright. MaCS detects faults in controllers and performs dynamic reconfiguration of the control system using steering.

Sanjit A. Seshia (This is joint work with Randal E. Bryant.) Carnegie Mellon University	Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods We present a new approach to unbounded, fully symbolic model checking of timed automata that is based on an efficient translation of quantified separation logic to quantified Boolean logic. The core operations of eliminating quantifiers over real variables and deciding the validity of separation logic formulas are respectively translated to eliminating quantifiers on Boolean variables and checking Boolean satisfiability (SAT). We can thus leverage well-known techniques for Boolean formulas, including Binary Decision Diagrams (BDDs) and recent advances in SAT and SAT-based quantifier elimination.

Oleg Sheyner Carnegie Mellon University	Generating Failure Scenario Graphs for LTL properties A scenario graph is a succinct representation of all execution paths through a system that violate some correctness property. Scenario graphs can be viewed as automata accepting a subset of the system's behavior. This perspective produces an algorithm for generating scenario graphs for any correctness property that can be specified in linear temporal logic.

Li Tan, Oleg Sokolsky, and Insup Lee University of Pennsylvania	Property-based test generation This poster shows our integreted efforts on applying model-checking techinque to the domain of testing. Our goal is to have the test generation centeralized on system properties. We use the techinque developed in model-checking community to model systems (CHARON), extract test specification from system propertries (An extension of nonvacuity) , extend the notion of "testable" properties (Is generally LTL property testable?), and generate efficient tests (Partial test derived from model checker's proof). We also discuss the issue of realizing test harness.

Ted Wong, Jeannette Wing, and Chennxi Wang Carnegie Mellon University	Hathor: A Storage System / VSR Prototype We present the design of a decentralized redistribution protocol for threshold-shared data and an analysis of its security and correctness properties. Decentralization avoids the introduction of a single point of failure in the protocol. We also present a performance evaluation of a prototype recovery service for survivable storage that utilizes the redistribution protocol.

Ted Wong, Jeannette Wing, and Chennxi Wang Carnegie Mellon University	Verifiable Secret Redistribution We present the design of a decentralized redistribution protocol for threshold-shared data and an analysis of its security and correctness properties. Decentralization avoids the introduction of a single point of failure in the protocol. We also present a performance evaluation of a prototype recovery service for survivable storage that utilizes the redistribution protocol.

Håkan Younes and Reid Simmons Carnegie Mellon University	Sampling-based Probabilistic Model Checking We present an algorithm for verifying CSL properties of stochastic discrete event systems. The algorithm is based on sequential acceptance sampling and discrete event simulation. We compare our algorithm with symbolic probabilistic model checking algorithms implemented in PRISM on three case studies, and show that our sampling-based algorithm scales better with the size of the state space and has lower memory requirements.


For program concerns, please contact Bruce Krogh <krogh@ece.cmu.edu>. For web site difficulties, please contact Margaret Weigand <weigand@cs.cmu.edu>.

[ Attendees ] [ Main Page ] [ Schedule ]
[Top of Page]	Updated: 16-May-03