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

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

引用

FORMAL ASPECTS OF COMPUTING 2023年第3期35卷 18-18页

作者： 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 Fasanengarten 5 D-76131 Karlsruhe Germany

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 article, 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

来源：评论

学校读者我要写书评

暂无评论

JML and OpenJML for java 16 23

JML and OpenJML for Java 16

引用

23rd ACM International Workshop on Formal Techniques for java-Like Programs (FTfJP)

作者： Cok, David R. Safer Software Consulting LLC Rochester NY 14610 USA

ISBN: (纸本)9781450385435

As the java language evolves, the java modeling language (JML) and the OpenJML deductive verification tool must evolve with it. Changes in java since java 8 bring language and organizational changes which affect the semantics of JML and the implementation of OpenJML. They also raise questions about language definition, joint efforts, and community engagement, some enumerated in this paper, for the java formal reasoning community to address.

关键词： java modeling language JML OpenJML software verification deductive verification

来源：评论

学校读者我要写书评

暂无评论

Teaching Design-by-Contract for the modeling and Implementation of Software Systems 14

Teaching Design-by-Contract for the Modeling and Implementat...

引用

14th International Conference on Software Technologies (ICSOFT)

作者： Ozkaya, Mert Yeditepe Univ Dept Comp Engn Istanbul Turkey

ISBN: (纸本)9789897583797

Defensive programming is considered as a software design approach that promotes the reliable software development via the considerations of different cases for the software modules. Design-by-Contract (DbC) applies defensive programming systematically in terms of contracts that are a pair of pre-conditions on the module input and post-conditions on the module output. In this paper, a DbC-based teaching methodology is proposed, which aims to teach undergraduate students how to use contracts for the modeling and implementation of software systems. The teaching methodology consists of three consecutive steps. Firstly, the students will learn how to model software architectures in terms of components and their communication links. The component behaviours are specified as contracts, which are attached to the messages that the components exchange. In the second step, the students will learn how to implement the contractual software architectures in java using java's assertion mechanisms in a way that the contractual design decisions are all preserved in the code. Lastly, the students will learn the java modeling language for combining the contractual modeling and java implementation in a single model to avoid any inconsistencies between the model and implementation and automatically verify the correctness of the implementation against the modeled behaviours.

关键词： java modeling language Defensive Programming Design-by-Contract Education

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：