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

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

来源：评论

学校读者我要写书评

暂无评论

Conformance test development with the java modeling language

Conformance test development with the Java modeling language

引用

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

作者： Sondergaard, Hans Korsholm, Stephan E. Ravn, Anders P. VIA Univ Coll Horsens Denmark Aalborg Univ Dept Comp Sci Aalborg Denmark

In order to claim conformance with a java Specification Request, a java implementation has to pass all tests in an associated Technology Compatibility Kit. This paper presents a model-based development of a Technology Compatibility Kit test suite and a test execution tool for the draft safety-critical java profile specification. The java modeling language is used to model conformance constraints for the profile. java modeling language annotations define contracts for classes and interfaces. The annotations are translated by a tool into runtime assertion checks. Hereby, the design and elaboration of the concrete test cases are simplified, because the expected results are derived from contracts and thus do not need to be provided explicitly. Bottom-up testing is applied for testing methods of the safety-critical java classes, whereas top-down testing is applied for testing global properties, such as protocols, memory management, and real-time properties, including scheduling. The tests are executed using a simplified version of JUnit, which makes the test suite executable on resource-constrained platforms. Copyright (c) 2017 John Wiley & Sons, Ltd.

关键词： test conformance test model-based testing Technology Compatibility Kit formal specification java modeling language safety-critical java real-time java

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Conformance test development with the java modeling language

引用

CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE 2017年第22期29卷

作者： Sondergaard, Hans Korsholm, Stephan E. Ravn, Anders P. VIA Univ Coll Horsens Denmark Aalborg Univ Dept Comp Sci Aalborg Denmark

关键词： test conformance test model-based testing Technology Compatibility Kit formal specification java modeling language safety-critical java real-time java

来源：评论

学校读者我要写书评

暂无评论

The java Verification Tool KeY:A Tutorial 26th

The Java Verification Tool KeY:A Tutorial

引用

26th International Symposium on Formal Methods (FM)

作者： Beckert, Bernhard Bubel, Richard Drodt, Daniel Haehnle, Reiner Lanzinger, Florian Pfeifer, Wolfram Ulbrich, Mattias Weigl, Alexander Karlsruhe Inst Technol Karlsruhe Germany Tech Univ Darmstadt Darmstadt Germany

ISBN: (纸本)9783031711763;9783031711770

The KeY tool is a state-of-the-art deductive program verifier for the java language. Its verification engine is based on a sequent calculus for dynamic logic, realizing forward symbolic execution of the target program, whereby all symbolic paths through a program are explored. Method contracts make verification scalable. KeY combines auto-active and fine-grained proof interaction, which is possible both at the level of the verification target and its specification, as well as at the level of proof rules and program logic. This makes KeY well-suited for teaching program verification, but also permits proof debugging at the source code level. The latter made it possible to verify some of the most complex java code to date. The article provides a self-contained introduction to the working principles and the practical usage of KeY for anyone with basic knowledge in logic and formal methods.

关键词： Program verification Deductive verification Dynamic Logic java modeling language

来源：评论

学校读者我要写书评

暂无评论

Verifying OpenJDK's LinkedList using KeY (extended paper)

引用

INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER 2022年第5期24卷 783-802页

作者： Hiep, Hans-Dieter A. Maathuis, Olaf Bian, Jinting de Boer, Frank S. de Gouw, Stijn Ctr Wiskunde & Informat CWI Amsterdam Netherlands Leiden Inst Adv Comp Sci LIACS Leiden Netherlands Open Univ OU Heerlen Netherlands Achmea Zeist Netherlands

As a particular case study of the formal verification of state-of-the-art, real software, we discuss the specification and verification of a corrected version of the implementation of a linked list as provided by the ... 详细信息

关键词： Deductive verification KeY java modeling language Case study Standard library Bug

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

An Aspect-Oriented Approach to Modular Behavioral Specification

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2006年第1期163卷 45-56页

作者： Yamada, Kiyoshi Watanabe, Takuo Natl Inst Adv Ind Sci & Technol Res Ctr Informat Secur Tokyo Japan Tokyo Inst Technol Dept Comp Sci Tokyo Japan

Behavioral interface specification languages, such as java modeling language (JML), can be used to specify the behavior of program modules. We have developed a behavioral interface specification language Moxa, an extension of JML. Moxa provides a new modularization mechanism called assertion aspect that can capture the crosscutting properties among assertions. In this paper, we briefly explain the notion of assertion aspects and the design of Moxa, and then we show an example specification. By comparing the specification to its JML counterpart, we show that the use of assertion aspects clarifies the large, complex specification and greatly simplifies each assertion in the specification.

关键词： Design by Contract Assertion Aspect java modeling language AspectJ

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：