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

25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) held as part of the 22nd European Joint Conferences on Theory and Practice of Software (ETAPS)

作者： Artho, Cyrille Visser, Willem KTH Royal Inst Technol EECS S-10044 Stockholm Sweden Univ Stellenbosch Dept Comp Sci Stellenbosch South Africa

This paper gives a brief overview of java pathfinder, or jpf-core. We describe the architecture of JPF, its strengths, and how it was set up for SV-COMP 2019.

ISBN: (纸本)9783030175023;9783030175016

This paper gives a brief overview of java pathfinder, or jpf-core. We describe the architecture of JPF, its strengths, and how it was set up for SV-COMP 2019.

关键词： java pathfinder Software model checking java program analysis

来源：评论

学校读者我要写书评

暂无评论

TOWARDS MODEL CHECKING WITH java pathfinder FOR AUTONOMIC SYSTEMS SPECIFIED AND GENERATED WITH ASSL

TOWARDS MODEL CHECKING WITH JAVA PATHFINDER FOR AUTONOMIC SY...

引用

4th International Conference on Software and Data Technologies

作者： Vassev, Emil Hinchey, Mike Quigley, Aaron Univ Coll Dublin Lero Irish Software Engn Res Ctr Dublin 2 Ireland Univ Limerick Lero Irish Software Engn Res Ctr Limerick Ireland

ISBN: (纸本)9789896740092

Autonomic computing has been recognized as a valid approach to the development of large-scale self-managing complex systems. The Autonomic System Specification Language (ASSL) is an initiative for the development of autonomic systems where we approach the problem of formal specification, validation, and code generation of such systems within a framework. As part of our research on ASSL, we have developed and investigated different approaches to software verification. Currently, the latter is possible via built-in consistency checking and functional testing where handling logical errors is a daunting task. In this paper, we discuss our work on model checking with NASA's java pathfinder tool, which is an explicit-state model checker that works directly on the generated java code. We propose optional automatic generation of test drivers in the form of pathfinder API calls seeded in the ASSL-generated code.

关键词： Autonomic Computing Model Checking ASSL java pathfinder

来源：评论

学校读者我要写书评

暂无评论

引用

13th International Conference on Quality Software (QSIC)

作者： Ibrahimov, Elmin Wang, Jixing Zhou, Zhi Quan Univ Wollongong Sch Comp Sci & Software Engn Wollongong NSW 2522 Australia

ISBN: (纸本)9780769550398

When a model checker cannot explore the entire state space because of limited resources, model checking becomes a kind of testing with an attempt to find a failure (violation of properties) quickly. We consider two state sequences in model checking: (i) the sequence in which new states are generated, and (ii) the sequence in which the states generated in sequence (i) are checked for property violation. We observe that neighboring states in sequence (i) often have similarities in certain ways. Based on this observation we propose a search strategy, which generates sequence (ii) in such a way that similar states are evenly spread over the sequence. As a result, neighboring states in sequence (ii) can have a higher diversity. A pilot empirical study with java pathfinder suggests that the proposed strategy can outperform random search in terms of creating equal or smaller number of states to detect a failure.

关键词： Model checking random search similarity-based search heuristics adaptive random sequence java pathfinder

来源：评论

学校读者我要写书评

暂无评论

Verifying Nested Lock Priority Inheritance in RTEMS with java pathfinder 18th

Verifying Nested Lock Priority Inheritance in RTEMS with Jav...

引用

18th International Conference on Formal Engineering Methods (ICFEM)

作者： Gadia, Saurabh Artho, Cyrille Bloom, Gedare Univ Southern Calif Los Angeles CA USA Natl Inst Adv Ind Sci & Technol Osaka Japan KTH Royal Inst Technol Stockholm Sweden Howard Univ Washington DC 20059 USA

ISBN: (纸本)9783319478463;9783319478456

Scheduling and synchronization algorithms for uniprocessor real-time systems benefit from the rich theory of schedulability analysis, and yet translating these algorithms to practical implementations can be challenging. This paper presents a java model of the priority inheritance protocol for mutual exclusion, as implemented in the RTEMS open-source real-time operating system. We verified this model using java pathfinder to detect potential data races, deadlocks, and priority inversions. JPF detected a known bug in the RTEMS implementation, which we modified along with the java model. Verification of the modified model showed the absence of data races, deadlocks, and established nine protocol-specific correctness properties.

关键词： java pathfinder RTEMS Priority inheritance

来源：评论

学校读者我要写书评

暂无评论

State Extensions for java pathfinder 08

State Extensions for Java PathFinder

引用

30th International Conference on Software Engineering

作者： Gvero, Tihomir Gligoric, Milos Lauterburg, Steven d'Amorim, Marcelo Marinov, Darko Khurshid, Sarfraz Univ Belgrade Belgrade Serbia

ISBN: (纸本)9781605580791

java pathfinder (JPF) is an explicit-state model checker for java programs. JPF implements a backtrackable java Virtual Machine (JVM) that provides non-deterministic choices and control over thread scheduling. JPF is itself implemented in java and runs on top of a host JVM. JPF represents the JVM state of the program being checked and performs three main operations on this state representation: bytecode execution, state backtracking, and state comparison. This paper summarizes four extensions that we have developed to the JPF state representation and operations. One extension provides a new functionality to JPF, and three extensions improve performance of JPF in various scenarios. Some of our code has already been included in publicly available JPF.

关键词： java pathfinder JPF delta execution mixed execution

来源：评论

学校读者我要写书评

暂无评论

Bounded model checking v nástroji java pathfinder

Bounded model checking v nástroji Java PathFinder

引用

作者： Dudka, Vendula Brno University of Technology

Diplomová práce je věnovaná aplikaci formální metody bounded model checking pro automatickou opravu chyb. Oprava se specializuje na chyby spojené se souběžností. Práce je zaměřena na programy napsané v jazyce java, a proto pro verifikační metodu byl zvolen model checker java pathfinder, který je určen pro java programy. Vlastní verifikační metoda spočívá v aplikaci strategie pro navigaci stavovým prostorem do místa verifikace. Z daného místa je spuštěn bounded model checking pro ověření opravy. Navigace stavovým prostorem je implementována pomocí strategie record&replay trace. Pro aplikaci bounded model checkingu jsou implementovány další parametry a moduly pro verifikaci speciálních vlastností systému, které ověřují koreknost opravy chyby. Bounded model checking se provádí v okolí opravy.

关键词： Model Checking java pathfinder Bounded model checking verifikace Record&Replay trace automatická oprava souběžnost ověřování opravy Model Checking java pathfinder Bounded model checking verification Record&Replay trace self-healing concurren

来源：评论

学校读者我要写书评

暂无评论

Debugger interface for java pathfinder model checker

Debugger interface for Java PathFinder model checker

引用

作者： Vávra, Štěpán Charles University of Prague

The aim of this work is to integrate java pathfinder into java Platform Debugger Architecture. That is, to allow using java pathfinder instead of a common java Virtual Machine for the purpose of debugging java applications in any modern java Integrated Development Environment with all its advantages such as various kinds of breakpoints, direct stepping in opened source files, and call stack and object inspection. The resulting work provides users with all the features they are used to while debugging java applications. None of this requires any external tools, editors or a complicated setup. Therefore, users are able to view, debug and understand the program state while replaying an error trace in java pathfinder. The key part of the study is an implementation of the java Debug Wire Protocol Agent as an extension for java pathfinder. That makes JPF more complete as a Virtual Machine in the eyes of the community and the java users in general. Powered by TCPDF (***)

关键词： debugging java pathfinder java Debug Wire Protocol Agent java Platform Debugger Architecture

来源：评论

学校读者我要写书评

暂无评论

Model checking agent programming languages

引用

AUTOMATED SOFTWARE ENGINEERING 2012年第1期19卷 5-63页

作者： Dennis, Louise A. Fisher, Michael Webster, Matthew P. Bordini, Rafael H. Univ Liverpool Dept Comp Sci Liverpool L69 3BX Merseyside England Virtual Engn Ctr Daresbury Lab Warrington WA4 4AD Cheshire England Univ Fed Rio Grande do Sul Inst Informat BR-91501970 Porto Alegre RS Brazil

In this paper we describe a verification system for multi-agent programs. This is the first comprehensive approach to the verification of programs developed using programming languages based on the BDI (belief-desire-intention) model of agency. In particular, we have developed a specific layer of abstraction, sitting between the underlying verification system and the agent programming language, that maps the semantics of agent programs into the relevant model-checking framework. Crucially, this abstraction layer is both flexible and extensible;not only can a variety of different agent programming languages be implemented and verified, but even heterogeneous multi-agent programs can be captured semantically. In addition to describing this layer, and the semantic mapping inherent within it, we describe how the underlying model-checker is driven and how agent properties are checked. We also present several examples showing how the system can be used. As this is the first system of its kind, it is relatively slow, so we also indicate further work that needs to be tackled to improve performance.

关键词： Multi-agent systems Agent programming languages BDI formal verification Model checking java pathfinder

来源：评论

学校读者我要写书评

暂无评论

Incremental State-Space Exploration for Programs with Dynamically Allocated Data 08

Incremental State-Space Exploration for Programs with Dynami...

引用

30th International Conference on Software Engineering

作者： Lauterburg, Steven Sobeih, Ahmed Marinov, Darko Viswanathan, Mahesh Univ Illinois Dept Comp Sci Urbana IL 61801 USA

ISBN: (纸本)9781605580791

We present a novel technique that speeds up state-space exploration (SSE) for evolving programs with dynamically allocated data. SSE is the essence of explicit-state model checking and an increasingly popular method for automating test generation. Traditional, non-incremental SSE takes one version of a program and systematically explores the states reachable during the program's executions to find property violations. Incremental SSE considers several versions that arise during program evolution: reusing the results of SSE for one version can speed up SSE for the next version, since state spaces of consecutive program versions can have significant similarities. We have implemented our technique in two model checkers: java pathfinder and the J-Sim state-space explorer. The experimental results on 24 program evolutions and exploration changes show that for non-initial runs our technique speeds up SSE in 22 cases from 6.43% to 68.62% (with median of 42.29%) and slows down SSE in only two cases for -4.71% and -4.81%.

关键词： State-space exploration incremental computation model checking java pathfinder JPF J-Sim

来源：评论

学校读者我要写书评

暂无评论

Addressing Challenges in Obtaining High Coverage When Model Checking Android Applications 24

Addressing Challenges in Obtaining High Coverage When Model ...

引用

24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software (SPIN)

作者： Botha, Heila Tkachuk, Oksana van der Merwe, Brink Visser, Willem Univ Stellenbosch Dept Comp Sci CSIR CAIRMeraka Stellenbosch South Africa NASA SGT Inc Ames Res Ctr Moffett Field CA 94035 USA Univ Stellenbosch Dept Comp Sci Stellenbosch South Africa

ISBN: (纸本)9781450350778

Current dynamic analysis tools for Android applications do not get good code coverage since they can only explore a subset of the behaviors of the applications and do not have full control over the environment in which they execute. In this work we use model checking to systematically explore application paths while reducing the analysis size using state matching and backtracking. In particular, we extend the java pathfinder (JPF) model checking environment for Android. We describe the dificulties one needs to overcome to make this a reality as well as our current approaches to handling these issues. We obtain significantly higher coverage using shorter event sequences on a representative sample of Android apps, when compared to Dynodroid and Sapienz, the current state-of-the-art dynamic analysis tools for Android applications.

关键词： Model Checking java pathfinder Android Applications Dynamic Analysis

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：