To increase the impact and capabilities of formal verification, it should be possible to apply different verification techniques on the same specification. However, this can only be achieved if verification tools agre...
详细信息
ISBN:
(数字)9783319989389
ISBN:
(纸本)9783319989389;9783319989372
To increase the impact and capabilities of formal verification, it should be possible to apply different verification techniques on the same specification. However, this can only be achieved if verification tools agree on the syntax and underlying semantics of the specification language and unfortunately, in practice, this is often not the case. In this paper, we concentrate on one particular example, namely java programs annotated with JML, and we present a case study in understanding differences in the treatment of these specifications. Concretely, we take a collection of JML-annotated programs, that we tried to reverify using KeY and OpenJML. This effort led to a list of syntactical and semantical differences in the JML support between KeY and OpenJML. We discuss these differences, and then derive some general principles on how to improve interoperability between verification tools, based on the experiences from this case study.
Extended Static Checking (ESC) is a fully automated formal verification technique. Verification in ESC is achieved by translating programs and their specifications into verification conditions (VCs). Proof of a VC est...
详细信息
Extended Static Checking (ESC) is a fully automated formal verification technique. Verification in ESC is achieved by translating programs and their specifications into verification conditions (VCs). Proof of a VC establishes the correctness of the program. The implementations of many seemingly simple algorithms are beyond the ability of traditional Extended Static Checking (ESC) tools to verify. Not being able to verify toy examples is often enough to turn users off of the idea of using formal methods. ESC4, the ESC component of the JML4 project, is able to verify many more kinds of methods in part because of its use of novel techniques which apply multiple theorem provers. In particular, we present Offline User-Assisted ESC (OUA-ESC), a new form of verification that lies between ESC and Full Static Program Verification (FSPV). ESC is generally quite efficient, as far as verification tools go, but it is still orders of magnitude slower than simple compilation. As can be imagined, proving VCs is computationally expensive: While small classes can be verified in seconds, verifying larger programs of 50 KLOC can take hours. To help address the added cost of using multiple provers and this lack of scalability, we present the multi-threaded version of ESC4 and its distributed prover back-end.
We give an account on the authors' experience and results from the software verification competition held at the Formal Methods 2012 conference. Competitions like this are meant to provide a benchmark for verifica...
详细信息
We give an account on the authors' experience and results from the software verification competition held at the Formal Methods 2012 conference. Competitions like this are meant to provide a benchmark for verification systems. It consisted of three algorithms which the authors have implemented in java, specified with the java modeling language, and verified using the KeY system. Building on our solutions, we argue that verification systems which target implementations in real-world programming languages better have powerful abstraction capabilities. Regarding the KeY tool, we explain features which, driven by the competition, have been freshly implemented to accommodate for these demands.
Android is one of the major smartphone platforms today. One reason for this success is that many interesting applications are made available through Google Play. The increasing functionality, however, entails new risk...
详细信息
Android is one of the major smartphone platforms today. One reason for this success is that many interesting applications are made available through Google Play. The increasing functionality, however, entails new risks. To defend against attacks, Android provides a sophisticated security architecture based on permissions which must be granted to applications at installation time. Since the Android source code is publicly available, the security community has the chance to assess the security mechanisms of Android. Due to its large code body, a completely manual code review is tedious, and hence, tool support for this task is desirable. As a first step in this direction, we propose to extract the implemented access control policy from the code for Android system services with the help of program slicing. After this abstraction phase, we analyze the extracted policy against the documentation. For this purpose, we use the java modeling language in conjunction with extended static checking. We applied this approach to core system services of Android 4.0.3 and identified some inconsistencies between the documentation and the implementation.
Safety-critical digital avionics systems are becoming increasingly complex. Consequently, exhaustive testing may be impossible or impractical to demonstrate that the software of these systems complies with airworthine...
详细信息
ISBN:
(纸本)9781450316880
Safety-critical digital avionics systems are becoming increasingly complex. Consequently, exhaustive testing may be impossible or impractical to demonstrate that the software of these systems complies with airworthiness requirements. Software development assurance in accordance with prescribed development standards is an accepted approach, but increases cost. These issues are addressed by the EU ARTEMIS CHARTER project. Its goals include managing system complexity, improving software quality, and reducing the total development effort. These goals have been achieved by a Quality Embedded Development (QED) approach, in which model-based development and Real-Time java are the key technologies. Tools have been developed to support development and verification activities. This paper presents CHARTER'S QED approach by taking examples from the development of a demonstrator for a safety-critical avionics system based on an aircraft Environmental Control System. The QED approach is assessed by comparing metrics that have been collected during the demonstrator development with metrics for conventional development. An important metric is the total development effort. The results indicate that a productivity improvement is achievable.
Canica is an integrated development environment for the java modeling language (JML), a formal behavioral interface specification language for java. The JML distribution includes several support tools, such as a synta...
详细信息
ISBN:
(纸本)9780889866423
Canica is an integrated development environment for the java modeling language (JML), a formal behavioral interface specification language for java. The JML distribution includes several support tools, such as a syntax checker, a compiler, and a document generator, and there are several third-party tools available for JML. However, most of these tools are command-line-based and work in isolation. Canica glues and streamlines these tools to provide a GUI-based, integrated environment for JML;for example, it automates unit testing including test data generation, test execution, and test result determination. In this paper, we describe the key features of Canica and explain its design and implementation. We also discuss the lessons that we learned from our development effort.
JML4 is an Eclipse-based Integrated Verification Environment for the java modeling language (JML) that supports several forms of verification, including Runtime Assertion Checking, Extended Static Checking (ESC), and ...
详细信息
ISBN:
(纸本)9781605586809
JML4 is an Eclipse-based Integrated Verification Environment for the java modeling language (JML) 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, but we provide an optimization for loops. A configurable Prover Coordinator allows the easy implementation of various proof strategies. Caching discharged VCs helps reduce the number of calls to the provers when reverifying code. Caches are not commonly used because of their fragility w.r.t. source code changes, but we propose a simple way to make them more resilient.
Design by Contract (DBC) is an oft-cited, but rarely followed, programming practice that focuses on writing formal specifications first, and writing code that fulfills those specifications second. The development of s...
详细信息
ISBN:
(纸本)9781424459124
Design by Contract (DBC) is an oft-cited, but rarely followed, programming practice that focuses on writing formal specifications first, and writing code that fulfills those specifications second. The development of static analysis tools over the past several years has made it possible to fully embrace DBC in java systems by writing, type checking, and consistency checking rich behavioral specifications for java before writing any code. This paper discusses a DEC-based, verification-centric software development process for java that integrates the Business Object Notation (BON), the java modeling language, and several associated tools including the BON compiler BONC, the ESC/java2 static checker, a runtime assertion checker, and a specification-based unit test generator. This verification-centric process, reinforced by its rich open source tool support, is one of the most advanced, concrete, open, practical, and usable processes available today for rigorously designing and developing software systems.
techniques are indispensable for the specification and veri. cation of the functional behaviour of programs. In object-oriented specification languages like java modeling language, a powerful abstraction technique is ...
详细信息
techniques are indispensable for the specification and veri. cation of the functional behaviour of programs. In object-oriented specification languages like java modeling language, a powerful abstraction technique is the use of model classes, that is, classes that are only used for specification purposes and that provide object-oriented interfaces for essential mathematical concepts such as sets or relations. Although the use of model classes in specifications is natural and powerful, they pose problems for veri. cation. Program verifiers map model classes to their underlying logics. Flaws in a model class or the mapping can easily lead to unsoundness and incompleteness. This article proposes an approach for the faithful mapping of model classes to mathematical structures provided by the theorem prover of the program veri. er at hand. Faithfulness means that a given model class semantically corresponds to the mathematical structure it is mapped to. This approach enables reasoning about programs specified in terms of model classes. It also helps in writing consistent and complete model-class specifications as well as in identifying and checking redundant specifications.
We present an initial link between Z and JML that has enabled us to use Z/Eves to prove theorems about JML classes. We have applied this to the JML type system and the java HashMap class from the java Collections Fram...
详细信息
ISBN:
(纸本)9783540752202
We present an initial link between Z and JML that has enabled us to use Z/Eves to prove theorems about JML classes. We have applied this to the JML type system and the java HashMap class from the java Collections Framework. We present and discuss the issues behind a more general strategy for translation in both directions between Z and JML. This work is a contribution to the Verified Software Repository, part of the Grand Challenge in Verified Software.
暂无评论