| 1: | Verifying the Microsoft Hyper-V Hypervisor with VCC |
| | Stephan Tobies |
| | Abstract: VCC is an industrial-strength verification suite for the formal verification of concurrent, system-level C code. VCC's development is driven by two major verification initiatives in the Verisoft XT project: the Microsoft Hyper-V Hypervisor and SYSGO's PikeOS micro kernel. The talk will present the challenges posed by the Hypervisor verification effort and how we have solved them with VCC. |
| 2: | Designing a Type System based on Static Analysis Principles |
| | Axel Simon |
| | Abstract: In this talk we illustrate the concepts of complete and condensing domains from the abstract interpretation literature and apply them to the task of designing a type system. Specifically, we argue that a complete abstraction corresponds to a type inference delivering principle types whereas the property of being condensing means that type inference can be done in a modular way. We then design a concurrent language that describes types using regular expressions and features full sub-typing. |
| 3: | Coping with Multi-thread Schedules |
| | Aarti Gupta |
| | Abstract: Effective techniques for verification of multi-threaded programs have to grapple with the central problem of an explosive number of thread schedules. In this talk, I will describe two main frameworks we have found useful in practice. The first is a static analysis framework for semantic reduction of thread interleavings, where we iteratively refine a transaction graph that captures the interleavings, by deriving sound invariants using abstract interpretation. For data race detection, this framework serves to reduce the number of false warnings captured by an initial lockset analysis, and facilitates the use of model checking on the remaining warnings to generate concrete error traces. The second framework combines dynamic testing with predictive analysis. Given a test execution of the multi-threaded program, we derive a symbolic predictive model to explore all (or some) alternative thread schedules over the same events. We model the inter-thread data flow, concurrency primitives, and correctness properties uniformly as happen-before constraints in our model. We use an SMT solver to find violations, performing an effective symbolic search over thread interleavings. |
| 4: | Overview and Industrial Applications of State Based Supervisory Control Synthesis |
| | Bert Van Beek |
| | Abstract: By means of supervisory control theory, controllers can be synthesized based on formal models of the uncontrolled plant and the control requirements. At the dawn of supervisory synthesis, the plant and control requirements were modeled as a set of, possibly synchronizing, finite automata. In state based supervisory control, control requirements can not only be specified by means of automata, but also by means of state exclusion and state-event exclusion. State exclusion allows the specification of safe or unsafe states in the plant. State-event exclusion restricts occurrence of events to certain states. Generalized state based control requirements are very suited to formally represent the informal control requirements that are defined by domain engineers in industry. Experience with this approach has shown the potential of an order of magnitude reduction of the specification and testing iteration loop. This is illustrated by means of a number of industrial applications in the domain of professional printing and copying machines and in the medical domain of MRI systems. The availability and performance of state-based supervisory control system tooling is discussed, and an overview is given of the work in several European projects on integration of tools for supervisory control synthesis with tools for verification, simulation and testing. |
| 5: | The Metro Rio ATP case study |
| | Alessio Ferrari and Alessandro Fantechi and Daniele Grasso and Gianluca Magnani |
| | Abstract: This paper reports on the Simulink/Stateflow based development of the on-board equipment of the Metr^o Rio Automatic Train Protection system. Particular focus is given to the strategies followed to address formal weaknesses and certification issues of the adopted tool-suite. On the development side, constraints on the Simulink/Stateflow semantics have been introduced and design practices have been adopted to gradually achieve a formal model of the system. On the verification side, a two-phase approach based on model based testing and abstract interpretation has been followed to enforce functional correctness and runtime error freedom. Quantitative results are presented to assess the overall strategy: the e ort required by the design activities is balanced by the e ectiveness of the verification tasks enabled by model based development and automatic code generation. |
| 6: | SMT-Based Formal Verification of a TTEthernet Synchronization Function |
| | Wilfried Steiner and Bruno Dutertre |
| | Abstract: TTEthernet is a communication infrastructure for mixed criticality systems that integrates dataflow from applications with different criticality levels on a single network. For applications of highest criticality, TTEthernet provides a synchronization strategy that tolerates multiple failures. The resulting fault-tolerant timebase can then be used for time-triggered communication to ensure temporal partitioning on the shared network. In this paper, we present the formal verification of the compression function which is a core element of the clock synchronization service of TTEthernet. The compression function is located in the TTEthernet switches: it collects clock readings from the end systems, performs a faulttolerant median calculation, and feedbacks the result to the end systems. While traditionally the formal proof of these types of algorithms is done by theorem proving, we successfully use the model checker sal-inf-bmc incorporating the YICES SMT solver. This approach improves the automatized verification process and, thus, reduces the manual verification overhead. |
| 7: | Model Checking the FlexRay Physical Layer Protocol |
| | Michael Gerke and Rüdiger Ehlers and Bernd Finkbeiner and Hans-Jörg Peter |
| | Abstract: The FlexRay standard, developed by a cooperation of leading companies in the automotive industry, is a robust communication protocol for distributed components in modern vehicles. In this paper, we present the first timed automata model of its physical layer protocol, and we use automatic verification to prove fault tolerance under several error models and hardware assumptions. The key challenge in the analysis is that the correctness of the protocol relies on the interplay of the bit-clock alignment mechanism with the precise timing behavior of the underlying asynchronous hardware. We give a general hardware model that is parameterized in low-level timing details such as hold times and propagation delays. Instantiating this model for a realistic design from the Nangate Open Cell Library, and verifying the resulting model using the real-time model checker Uppaal, we show that the communication system meets, and in fact exceeds, the fault-tolerance guarantees claimed in the FlexRay specification. |
| 8: | A Formal Model of Identity Mixer |
| | Jan Camenisch and Sebastian Mödersheim and Dieter Sommer |
| | Abstract: Identity Mixer is an anonymous credential system developed at IBM that allows users for instance to prove that they are over 18 years old without revealing their name or birthdate. This privacy-friendly technology is realized using zero-knowledge proofs. We describe a formal model of Identity Mixer that is well-suited for automated protocol verification tools in the spirit of black-box cryptography models. |
| 9: | Range Analysis of Microcontroller Code using Bit-Level Congruences |
| | Joerg Brauer and Andy King and Stefan Kowalewski |
| | Abstract: Verifying the correctness of microcontroller programs in presence of bitwise instructions, loops, and indirect data access is a challenging task. On microcontrollers such as the ATMEL ATmega16, it is necessary to show that an indirect write does not mutate registers, which are indirectly addressable. To prove this property, among others, this paper presents a relational binary-code semantics and details how this can be used to compute program invariants in terms of bit-level congruences. Moreover, it demonstrates how congruences can be combined with intervals to derive accurate ranges, as well as information about strided indirect memory accesses. |
| 10: | Correctness of Sensor Network Applications by Software Bounded Model Checking |
| | Frank Werner and David Faragó |
| | Abstract: We investigate the application of the software bounded model checking tool CBMC to the domain of wireless sensor networks (WSNs). We automatically generate a software behavior model from a network protocol (ESAWN) implementation in a WSN development and deploy- ment platform (TinyOS), which is used to rigorously verify the protocol. Our work is a proof of concept that automatic verification of programs of practical size (about 21 000 LoC) and complexity is possible with CBMC and can be integrated into TinyOS. The developer can automatically check for pointer dereference and array index out of bound errors. She can also check additional, e.g., functional, properties that she provides by assume- and assert-statements. This experience paper shows that our approach is in general feasible since we managed to verify about half of the prop- erties. We made the verification process scalable in the size of the code by abstraction (eg, from hardware) and by simplification heuristics. The latter also achieved scalability in data type complexity for the proper- ties that were verifiable. The others require technical advancements for complex data types within CBMC's core. |
| 11: | Automatic Error Correction of Java Programs |
| | Christian Kern and Javier Esparza |
| | Abstract: We present a technique for automatically detecting and correcting software bugs. The programmer is required to define a catalog of hotspots, syntactic constructs she considered to be error prone (e.g. i < N), together with suitable alternatives (e.g. i < (N + 1) and i < (N - 1)). Given a faulty program, search techniques are then applied to find a combination of alternatives yielding a correct program. The technique is implemented on top of the Java Pathfinder Framework. |
| 12: | Practical Issues with Formal Specifications Lessons Learned from an Industrial Case Study |
| | Michael Altenhofen and Achim D. Brucker |
| | Abstract: Many software companies still seem to be reluctant to use formal specifications in their development processes. Nevertheless, the trend towards implementing critical business applications in distributed environments makes such applications an attractive target for formal methods. Additionally, the rising complexity also increases the willingness of the development teams to apply formal techniques. In this paper, we report on our experiences in formally specifying several core components of one of our commercially available products. While writing the formal specification, we experienced several issues that had a noticeable consequences on our work. While most of these issues can be attributed to the specific method and tools we have used, we do consider some of the problems as more general, impeding the practical application of formal methods, especially by non-experts, in large scale industrial development. |
| 13: | Embedded Network Protocols for Mobile Devices |
| | Despo Galataki and Andrei Radulescu and Kees Verstoep and Wan Fokkink |
| | Abstract: Embedded networks for chip-to-chip networks are emerging as communication infrastructure in mobile devices. We present three novel embedded network protocols: a sliding window protocol, a protocol for opening and closing connections, and a bandwidth reservation protocol. The design of these protocols is tailored to the low power and low cost requirements of mobile devices. The model checker SPIN played an important role in the design and analysis of these protocols. Large instances of the protocols could be analyzed successfully using the distributed model checker DiVinE. |
| 14: | Formal analysis of BPMN models using Event-B |
| | Wei Wei and Jeremy W. Bryans |
| | Abstract: The use of business process models has gone far beyond documentation purposes. In the development of business applications, they can play the role of an artifact on which high level properties can be verified and design errors can be revealed in an e ort to reduce overhead at later software development and diagnosis stages. This paper demonstrates how formal verification may add value to the specification, design and development of business process models in an industrial setting. The analysis of these models is achieved via an algorithmic translation from the de-facto standard business process modeling language BPMN to Event-B, a widely used formal language supported by the Rodin platform which o ers a range of simulation and verification technologies. |
| 15: | Developing mode-rich satellite software by refinement in Event B |
| | Alexei Iliasov and Elena Troubitsyna and Linas Laibinis and Alexander Romanovsky and Kimmo Varpaaniemi and Dubravka Ilic and Timo Latvala |
| | Abstract: To ensure dependability of on-board satellite systems, the designers should, in particular, guarantee correct implementation of the mode transition scheme, i.e., ensure that the states of the system components are consistent with the global system mode. However, there is still a lack of scalable approaches to formal verification of correctness of complex mode transitions. In this paper we present a formal development of an Attitude and Orbit Control System (AOCS) undertaken within the ICT DEPLOY project. AOCS is a complex mode-rich system, which has an intricate mode-transition scheme. We show that refinement in Event B provides the engineers with a scalable formal technique that enables both development of mode-rich systems and proof-based verification of their mode consistency. |
| 16: | A Study of Shared-Memory Mutual Exclusion Protocols using CADP |
| | Radu Mateescu and Wendelin Serwe |
| | Abstract: Mutual exclusion protocols are an essential building block of concurrent systems: indeed, such a protocol is required whenever a shared resource has to be protected against concurrent non-atomic accesses. Hence, many variants of mutual exclusion protocols exist in the shared-memory setting, such as Petersons or Dekkers well-known protocols. Although the functional correctness of these protocols has been studied extensively, relatively little attention has been paid to their nonfunctional aspects, such as their performance in the long run. In this paper, we report on experiments with the performance evaluation of mutual exclusion protocols using Interactive Markov Chains. Steady-state analysis provides an additional criterion for comparing protocols, which complements the verification of their functional properties. We also carefully re-examined the functional properties, whose accurate formulation as temporal logic formulas in the action-based setting turns out to be quite involved. |
| 17: | Automatic Structure-based Code Generation from Coloured Petri Nets: A Proof of Concept |
| | Lars Kristensen and Michael Westergaard |
| | Abstract: Automatic code generation based on Coloured Petri Net (CPN) models is challenging because CPNs allow for the construction of abstract models that intermix control flow and data processing, making translation into conventional programming constructs difficult.We introduce Process-Partitioned CPNs (PP-CPNs) which is a subclass of CPNs equipped with an explicit separation of process control flow, message passing, and access to shared and local data. We show how PP-CPNs caters for a four phase structure-based automatic code generation process directed by the control flow of processes. The viability of our approach is demonstrated by applying it to automatically generate an Erlang implementation of the Dynamic MANET On-demand (DYMO) routing protocol specified by the Internet Engineering Task Force (IETF). |
| 18: | An Automated Translator for Model Checking Time Constrained Workflow Systems |
| | Ahmed Mashiyat and Fazle Rabbi and Hao Wang and Wendy MacCaull |
| | Abstract: Workflows have proven to be a useful conceptualization for the automation of business processes. While formal verification methods (e.g., model checking) can help ensure the reliability of workflow systems, the industrial uptake of such methods has been slow largely due to the effort involved in modeling and the memory required to verify complex systems. Incorporation of time constraints in such systems exacerbates the latter problem. We present an automated translator, YAWL2DVE-t, which takes as input a time constrained workflow model built with the graphical modeling tool YAWL, and outputs the model in DVE, the system specification language for the distributed LTL model checker DiVinE. The automated translator, together with the graphical editor and the distributed model checker, provides a method for rapid design, verification and refactoring of time constrained workflow systems. We present a realistic case study developed through collaboration with the local health authority. |
![[Valid RSS]](./images/valid-rss.png "Validate my RSS feed")