检索结果-内蒙古大学图书馆

Reasoning About JML: Differences Between KeY and OpenJML 1

14th International Conference on Integrated Formal Methods (IFM)

作者： Boerman, Jan Huisman, Marieke Joosten, Sebastiaan Univ Twente Enschede Netherlands

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.

关键词： java modeling language Static verification OpenJML KeY

来源：评论

学校读者我要写书评

暂无评论

Faster and More Complete Extended Static Checking for the java modeling language

引用

JOURNAL OF AUTOMATED REASONING 2010年第1-2期44卷 145-174页

作者： James, Perry R. Chalin, Patrice Concordia Univ Dept Comp Sci & Software Engn Dependable Software Res Grp Montreal PQ Canada

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.

关键词： Extended static checking Static verification Theorem provers java modeling language JML4 ESC ESC4

来源：评论

学校读者我要写书评

暂无评论

Implementation-level verification of algorithms with KeY

引用

INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER 2015年第6期17卷 729-744页

作者： Bruns, Daniel Mostowski, Wojciech Ulbrich, Mattias Karlsruhe Inst Technol D-76127 Karlsruhe Germany Univ Twente NL-7500 AE Enschede Netherlands

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.

关键词： Formal verification Benchmark java modeling language Theorem prover

来源：评论

学校读者我要写书评

暂无评论

Understanding the implemented access control policy of Android system services with slicing and extended static checking

引用

INTERNATIONAL JOURNAL OF INFORMATION SECURITY 2015年第4期14卷 347-366页

作者： Mustafa, Tanveer Sohr, Karsten Univ Bremen D-28359 Bremen Germany

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.

关键词： Android Slicing java modeling language Extended static checking

来源：评论

学校读者我要写书评

暂无评论

Using CHARTER tools to develop a Safety-Critical Avionics Application in java 12

Using CHARTER tools to develop a Safety-Critical Avionics Ap...

引用

10th International Workshop on java Technologies for Real-Time and Embedded Systems (JTRES)

作者： Wedzinga, G. Wiegmink, K. Natl Aerosp Lab NLR Anthony Fokkerweg 2 NL-1059 CM Amsterdam Netherlands Natl Aerosp Lab NLR NL-8316 PR Marknesse Netherlands

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.

关键词： Safety Critical Avionics Systems Software Life-Cycle Real-Time java java modeling language Code Generation Formal Verification Resource Analysis Test Case Generation

来源：评论

学校读者我要写书评

暂无评论

Canica: An ide for the java modeling language

Canica: An ide for the Java Modeling Language

引用

10th IASTED International Conference on Software Engineering and Applications

作者： Perez, Angelica B. Cheon, Yoonsik Gates, Ann Q. Univ Texas Dept Comp Sci El Paso TX 79968 USA

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.

关键词： integrated development environment specification tool programming tool unit test java modeling language

来源：评论

学校读者我要写书评

暂无评论

ESC4: A Modern Caching ESC for java

ESC4: A Modern Caching ESC for Java

引用

8th Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2009)

作者： James, Perry R. Chalin, Patrice Concordia Univ Dept Comp Sci & Software Engn Montreal PQ Canada

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.

关键词： java modeling language JML4 ESC4

来源：评论

学校读者我要写书评

暂无评论

A Verification-centric Software Development Process for java

A Verification-centric Software Development Process for Java

引用

9th International Conference on Quality Software (QSIC 2009)

作者： Zimmerman, Daniel M. Kiniry, Joseph R. Univ Washington Inst Technol Tacoma WA 98402 USA Univ Coll Dublin Sch Comp Sci & Informat Dublin Ireland

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.

关键词： software verification software engineering process formal methods Design by Contract java java modeling language Business Object Notation

来源：评论

学校读者我要写书评

暂无评论

Faithful mapping of model classes to mathematical structures

引用

IET SOFTWARE 2008年第6期2卷 477-499页

作者： Darvas, A. Mueller, P. ETH Dept Comp Sci CH-8092 Zurich Switzerland

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.

关键词： reasoning about programs functional behaviour specification formal specification java modeling language Diagnostic, testing, debugging and evaluating systems mathematical structures object-oriented specification languages program verifiers map model functional behaviour verification abstraction techniques Object-oriented programming object-oriented programming Formal methods model classes object-oriented interfaces

来源：评论

学校读者我要写书评

暂无评论

Proving theorems about JML classes

Proving theorems about JML classes

引用

Symposium on Formal Methods and Hybrid Real-Time Systems held in Honour of Dines Bjorner/Zhou Chaochen

作者： Freitas, Leo Woodcock, Jim Univ York Dept Comp Sci York YO10 5DD N Yorkshire England

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.

关键词： Grand Challenge in Verified Software JML java Collections Framework java HashMap class java modeling language formal specification linking theories mechanical theorem proving software verification Verified Software Repository Z Z/Eves

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：