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

Improving the Quality of Web-based Enterprise Applications with Extended Static Checking: A Case Study

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2006年第2期157卷 119-132页

作者： Rioux, Frederic Chalin, Patrice Concordia Univ Dept Comp Sci & Software Engn DSRG Montreal PQ Canada

ESC/java2 is a tool that statically detects errors in java programs and that uses the java modeling language (JML) as its annotation language. ESC/java2 can modularly reason about the code of a java Web-based Enterprise Application (WEA) and uncover potential errors. In this paper, we assessed the effectiveness of ESC/java2 at helping developers increase WEA quality by detecting design and implementation issues.

关键词： Web-based Enterprise Application Extended Static Checking Design by Contract 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

来源：评论

学校读者我要写书评

暂无评论

JML-Testing-Tools: A symbolic animator for JML specifications using CLP

引用

11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

作者： Bouquet, F Dadeau, F Legeard, B Utting, M Univ Franche Comte CNRS INRIA Lab Informat LIFC F-25030 Besancon France

ISBN: (纸本)3540253335

This paper describes a tool for symbolically animating JML specifications using Constraint Logic Programming. A customized solver handles constraints that represent the value of instance fields. We have extended a model-based approach to be able to handle object-oriented specifications. Our tool is also able to check properties during the simulation and exhibit counter-examples for false properties. Therefore, it can be used both for semi-automated verification and for validation purposes.

关键词： java modeling language model-based object-oriented symbolic animation

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Checking JML specifications with B machines

引用

4th International Conference of B and Z Users

作者： Bouquet, F Dadeau, F Groslambert, J Univ Franche Comte CNRS INRIA Lab Informat F-25030 Besancon France

ISBN: (纸本)3540255591

This paper presents a solution to the lack of tool-support for the JML models verification. We propose an approach for expressing JML specifications within the B abstract machines notation. The B machines generated from the JML can then be checked to ensure their correctness. Thus, we deduce the correctness of the original JML specification, ensured by rewriting rules which give the semantical equivalence of the two models. More generally, this translation can be applied to object-oriented specification languages using before-after predicates.

关键词： java modeling language JML object-oriented B method specifications abstract machines

来源：评论

学校读者我要写书评

暂无评论

Translating Natural language Requirements to Formal Specifications: A Study on GPT and Symbolic NLP 53

Translating Natural Language Requirements to Formal Specific...

引用

53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)

作者： Leong, Iat Tou Barbosa, Raul Univ Coimbra CISUC Dept Informat Engn Coimbra Portugal

ISBN: (纸本)9798350325430

Software verification is essential to ensure dependability and that a system or component fulfils its specified requirements. Natural language is the most common way of specifying requirements, although many verification techniques such as theorem proving depend upon requirements being written in formal specification languages. Automatically translating requirements into a formal specification language is a relevant and challenging research question, because developers often lack the necessary expertise. In our work we consider the application of natural language processing (NLP) to address that research question. This paper considers two distinct approaches to formalise natural language requirements: a symbolic method and a GPT-based method. The two methods are evaluated with respect to their ability to generate accurate java modeling language (JML) from textual requirements, and the results show good promise for automatic formalisation of requirements.

关键词： Software engineering Formal specification Software verification java modeling language

来源：评论

学校读者我要写书评

暂无评论

Formal Specification and Verification of JDK's Identity Hash Map Implementation 17th

Formal Specification and Verification of JDK's Identity Hash...

引用

17th International Conference on Integrated Formal Methods (IFM)

作者： de Boer, Martin de Gouw, Stijn Klamroth, Jonas Jung, Christian Ulbrich, Mattias Weigl, Alexander Open Univ Heerlen Netherlands FZI Res Ctr Informat Technol Karlsruhe Germany Karlsruhe Inst Technol Karlsruhe Germany

ISBN: (纸本)9783031077272;9783031077265

Hash maps are a common and important data structure in efficient algorithm implementations. Despite their wide-spread use, real-world implementations are not regularly verified. In this paper, we present the first case study of the IdentityHashMap class in the java JDK. We specified its behavior using the java modeling language (JML) and proved correctness for the main insertion and lookup methods with KeY, a semi-interactive theorem prover for JML-annotated java programs. Furthermore, we report how unit testing and bounded model checking can be leveraged to find a suitable specification more quickly. We also investigated where the bottlenecks in the verification of hash maps lie for KeY by comparing required automatic proof effort for different hash map implementations and draw conclusions for the choice of hash map implementations regarding their verifiability.

关键词： Real-world case study Deductive program verification java modeling language Verified hash map Verified data structure Cooperative verification

来源：评论

学校读者我要写书评

暂无评论

Abstraction in Deductive Verification: Model Fields and Model Methods 11th

Abstraction in Deductive Verification: Model Fields and Mode...

引用

11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation

作者： Cok, David R. Leavens, Gary T. Safer Software Consulting Rochester NY 14606 USA Univ Cent Florida Orlando FL 32816 USA

ISBN: (纸本)9783031198489;9783031198496

This Experience report compares using model fields and model methods for specifying abstractions in abstract implementations. Our experience is connected to past discussions of alternatives in modeling heap state changes and the axiomatic basis for deductive verification of programs with uninterpreted, underspecified or recursive methods.

关键词： Formal methods SMT solver Deductive verification java modeling language JML OpenJML

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：