Abstracts SAVCBS 2009
Key-note talk:
Compositional dependability modeling using ARCADE
Mariëlle Stoelinga University of Twente, The Netherlands
Dependability is a key concern for today's complex computer and
communication systems. To make sure that such an application
meets all its dependability requirements, a rigorous and systematic
analysis is required.
This talk introduces ARCADE, a formally well-rooted and extensible
framework for dependability evaluation. It has been designed so as to
combine the strengths of previous approaches to the evaluation of
dependability. Key feature is its formal semantics in terms of
Input/Output-Interactive Markov Chains, which enables both
compositional modeling and compositional analysis, enabling great
computational reductions for many models. The ARCADE approach is also
extensible, and hence adaptable to new circumstances or application
areas.
In this talk, I will introduce the new modeling approach, discuss its
formal semantics and illustrate its use with two case studies
Component-Based Semantics
Peter Mosses, Swansea University, UK
Formal semantic descriptions have many potential pragmatic advantages
over informal descriptions. Unfortunately, however, the major
frameworks for formal semantics do not support component-based
descriptions of programming languages. Different languages often have
many constructs in common, but the corresponding parts of their
semantic descriptions are not generally reusable. The lack of reusable
components is one of the reasons why it takes an immense effort to
give a semantic description of any larger language.
Here, we consider two semantic frameworks that do support
component-based language description: action semantics, and modular
structural operational semantics (MSOS). We analyse how the semantics
of individual constructs can be described independently in these
frameworks, explaining the key insights. We also speculate on the
possible applicability of similar techniques in component-based
software development.
Typestate Protocol Specification in JML
Taekgoo Kim, Carnegie Mellon University, USA
Kevin Bierhoff, Carnegie Mellon University, USA
Jonathan Aldrich, Carnegie Mellon University, USA
Sungwon Kang, Carnegie Mellon University, USA
The Java Modeling Language (JML) is a language for specifying the
behavior of Java source code. However, it can only implicitly describe
the protocols of Java classes and interfaces. Typestate protocol
specification is a lightweight and abstract way of presenting usage
protocols for object-oriented programs. In this paper, we propose a
technique for incorporating the typestate concept into JML for
specifying protocols of Java classes and interfaces, based on our
previous research on typestate protocol specification [4]. This paper
presents a set of formal translation rules for encoding typestate
protocol specifications into pre/post-condition specifications. It
also presents a way of supporting mixed use of typestate protocol
specifications and pre/post-condition specifications and how violation
of code contracts in inheritance can be handled. Finally, our proposed
technique is demonstrated within the Java/JML environment to show its
efficacy.
ESC4: A Modern Caching ESC for Java
Perry R. James, Concordia University, Canada
Patrice Chalin, Concordia University, Canada
JML4 is an Eclipse-based Integrated Verification Environment for the Java
Modeling Language that supports several forms of verification, including Runtime
Assertion Checking, Extended Static Checking (ESC), and Full Static Program
Verification. The first of these developed was ESC4, JML4's ESC component. This
paper presents its architecture. ESC4's verification-condition (VC) generation is
based on the approach described by Barnett and Leino for verifying unstructured
code, but we provide an optimized handling of structured loops. A
configurable Prover Coordinator is used to allow the implementation of various
proof strategies. Caching discharged VCs is integral to reducing the number of
calls to the provers when reverifying code. Typically caches are not used
because of their fragility w.r.t. source code changes, but we propose a simple
fix to make them more resilient.
A Framework for Estimating the Energy Consumption Induced by a
Distributed System's Architectural Style
Chiyoung Seo, University of Southern California, USA
George Edwards, University of Southern California, USA
Daniel Popescu, University of Southern California, USA
Sam Malek, George Mason University, USA
Nenad Medvidovic, University of Southern California, USA
The selection of an architectural style for a given software system is
an important factor in satisfying its quality requirements. In
battery-powered environments, such as mobile and pervasive systems,
efficiency with respect to energy consumption has gained prominence as
an important quality requirement. In this paper, we present a
framework that facilitates early estimation of the energy consumption
induced by an architectural style in a distributed system, and enables
an engineer to use energy consumption estimates along with other
quality attributes in determining the most appropriate style for a
given distributed application. We apply the framework to three
architectural styles, and evaluate it for precision and accuracy using
a middleware platform that supports the implementation of those
styles. In a large number of application scenarios, our framework
exhibited excellent precision, in that it was consistently able to
correctly rank the styles and estimate the relative differences in
their energy costs. Moreover, the framework has also proven to be
accurate: its estimates were within 7% of each style implementation's
actual energy cost.
Invited talk:
The Synergy of Precise and Fast Abstractions for Program Verification
N. Sharygina, University of Lugano
S. Tonetta, University of Lugano
A. Tsitovich, University of Lugano
Predicate abstraction is a powerful technique to reduce the state
space of a program to a finite and affordable number of states. It
produces a conservative over-approximation where concrete states are
grouped together according to a given set of predicates. A precise
abstraction contains the minimal set of transitions with regards to
the predicates, but as a result is computationally expensive. Most
model checkers therefore approximate the abstraction to alleviate the
computation of the abstract system by trading off precision with
cost. However, approximation results in a higher number of refinement
iterations, since it can produce more false counterexamples than its
precise counterpart. The refinement loop can become prohibitively
expensive for large programs.
In this talk I will present a new abstraction refinement technique
that combines slow and precise predicate abstraction techniques with
fast and imprecise ones. It allows computing the abstraction quickly,
but keeps it precise enough to avoid too many refinement
iterations. We implemented the new algorithm in our software model
checker, SATABS. Our tests with various real life benchmarks show that
the new approach almost systematically outperforms both precise and
imprecise techniques.
Marieke Huisman, Jonathan Aldrich,
Mike Barnett, Dimitra Giannakopoulou,
Gary T. Leavens, and Natasha Sharygina
