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

您好，读者！请登录

内蒙古大学图书馆

首页
概况
党建
资源
服务
科研支持
- 论文收录引用证明
- 科技查新
知识产权
档案馆
帮助

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

当前已输入0个字，您还可以输入200个字

全部搜索
期刊论文
图书
学位论文
标准
纸本馆藏
外文资源发现
数据库导航
超星发现

高级检索

时间限定

出版年份：

文献类型

图书期刊文献学位论文多媒体

馆藏选择

电子馆藏纸本馆藏

核心期刊

全部期刊 SCI 收录期刊 SSCI 收录期刊 EI 收录期刊 CSCD 收录期刊 CSSCI 收录期刊

语言

中文英文

文献类型

期刊文献图书学位论文标准纸本馆藏

帮助

文字说明：

T=题名（书名、题名），A=作者（责任者），K=主题词，P=出版物名称，PU=出版社名称，O=机构（作者单位、学位授予单位、专利申请人），L=中图分类号，C=学科分类号，U=全部字段，Y=年（出版发行年、学位年度、标准发布年）

检索规则说明：

AND代表“并且”；OR代表“或者”；NOT代表“不包含”；(注意必须大写,运算符两边需空一格)

检索范例：

范例一：(K=图书馆学 OR K=情报学) AND A=范并思 AND Y=1982-2016
范例二：P=计算机应用与软件 AND (U=C++ OR U=Basic) NOT K=Visual AND Y=2011-2016

分类表

所选分类

>> <<

限定检索结果

文献类型

20 篇 会议
3 篇 期刊文献
3 篇 学位论文

馆藏范围

26 篇 电子文献
0 种 纸本馆藏

日期分布

学科分类号

22 篇 工学
- 17 篇 软件工程
- 15 篇 计算机科学与技术...
- 3 篇 电气工程
- 2 篇 信息与通信工程
- 2 篇 控制科学与工程
3 篇 理学
- 2 篇 数学
- 1 篇 系统科学
1 篇 管理学
- 1 篇 管理科学与工程(可...

主题

26 篇 java pathfinder
16 篇 model checking
3 篇 jpf
3 篇 software model c...
2 篇 wilderness searc...
2 篇 design validatio...
2 篇 unmanned aerial ...
2 篇 user datagram pr...
2 篇 human machine in...
2 篇 fault protection
2 篇 sysml
2 篇 verification
2 篇 statechart
2 篇 model execution
1 篇 random search
1 篇 souběžnost
1 篇 android applicat...
1 篇 (probabilistic) ...
1 篇 complex systems
1 篇 defect discovery

机构

2 篇 chiba univ chiba
2 篇 univ tokyo
2 篇 aist risec amaga...
2 篇 univ stellenbosc...
1 篇 nasa ames resear...
1 篇 univ waterloo wa...
1 篇 univ west bohemi...
1 篇 howard univ wash...
1 篇 univ southern ca...
1 篇 european so obse...
1 篇 university of li...
1 篇 durham universit...
1 篇 european souther...
1 篇 charles univ pra...
1 篇 univ oxford oxfo...
1 篇 univ limerick le...
1 篇 inst politecn le...
1 篇 university of li...
1 篇 engn res ctr mob...
1 篇 computer science...

作者

4 篇 artho cyrille
2 篇 yamamoto mitsuha...
2 篇 visser willem
2 篇 marinov darko
2 篇 hagiya masami
2 篇 sebih nazim
2 篇 tanabe yoshinori
2 篇 lauterburg steve...
2 篇 weitl franz
1 篇 parizek pavel
1 篇 botha heila
1 篇 john day
1 篇 corrina gibson
1 篇 yokoyama shoichi
1 篇 tj gledhill
1 篇 欧阳志强
1 篇 rafael h. bordin...
1 篇 viswanathan mahe...
1 篇 potuzak tomas
1 篇 zhou zhi quan

语言

23 篇 英文
3 篇 中文

检索条件"主题词=Java Pathfinder"

共 26 条记录，以下是11-20 订阅

全选清除本页清除全部题录导出标记到"检索档案"

详细简洁

排序：

Abstractions for Executable and Checkable Fault Management Models

Abstractions for Executable and Checkable Fault Management M...

引用

Conference on Systems Engineering Research

作者： Gibson, Corrina Karban, Robert Andolfato, Luigi Day, John CALTECH Jet Prop Lab Pasadena CA 91011 USA European So Observ D-85748 Garching Germany

The work presented in this paper describes an approach used to develop SysML modeling patterns to express the logical behavior of fault protection (FP), test the model's logic via fault injection simulations, and verify the system's logical design via model checking. A FP model was architected with collaborating Statecharts that captures interactions between relevant system components (error monitors, FP engine, devices) and system behavior abstractions. Development of a method to implement verifiable and lightweight executable FP models enables future missions to have access to larger fault test domains and verifiable design patterns. (C) 2014 The Authors. Published by Elsevier B. V.

关键词： Model Checking Model execution java pathfinder SysML Statechart Fault Protection Design Validation

来源：评论

学校读者我要写书评

暂无评论

Probabilistic Model Checking of Randomized java Code 27th

Probabilistic Model Checking of Randomized Java Code

引用

27th International Symposium on Model Checking Software (SPIN)

作者： Fatmi, Syyeda Zainab Chen, Xiang Dhamija, Yash Wildes, Maeve Tang, Qiyi van Breugel, Franck York Univ Toronto ON Canada Univ Waterloo Waterloo ON Canada McGill Univ Montreal PQ Canada Univ Oxford Oxford England

ISBN: (纸本)9783030846299;9783030846282

java pathfinder (JPF) and PRISM are the most popular model checkers for java code and systems that exhibit random behaviour, respectively. Our tools make it possible to use JPF and PRISM together. For the first time, probabilistic properties of randomized algorithms implemented in a modern programming language can be checked. Furthermore, our tools are accompanied by a large collection of randomized algorithms that we implemented in java. From those java applications and with the help of our tools, we have generated the largest collection of realistic labelled (discrete time) Markov chains.

关键词： (Probabilistic) model checking java pathfinder PRISM

来源：评论

学校读者我要写书评

暂无评论

Partial verification of software components: Heuristics for environment construction

Partial verification of software components: Heuristics for ...

引用

33rd EUROMICRO Conference on Software Engineering and Advanced Applications

作者： Parizek, Pavel Plasil, Frantisek Charles Univ Prague Fac Math & Phys Dept Software Engn Malostranske Namesti 25 Prague 11800 1 Czech Republic Acad Sci Czech Republic Inst Comp Sci Prague Czech Republic

ISBN: (纸本)9780769529776

Code model checking of software components suffers from the well-known problem of state explosion when applied to highly parallel components, despite the fact that a single component typically comprises a smaller state space than the whole system. We present a technique that mitigates the problem of state explosion in code checking of primitive components with the java pathfinder in case the checked property is absence of concurrency errors. The key idea is to reduce parallelism in the calling protocol oil the basis of the information provided by static analysis searching for concurrency-related patterns in the component code;by a heuristic, some of the pattern instances are denoted as "suspicious". Then, the environment (needed to be available since java pathfinder checks only complete programs) is gene rated from a reduced calling protocol so that it exercises in parallel only those parts of the component's code that likely contain concurrency errors.

关键词： software components model checking concurrency errors java pathfinder static analysis

来源：评论

学校读者我要写书评

暂无评论

Comparing Metaheuristic Algorithms for Error Detection in java Programs

引用

3rd International Symposium on Search-Based Software Engineering, SSBSE 2011

作者： Chicano, Francisco Ferreira, Marco Alba, Enrique Univ Malaga E-29071 Malaga Spain Inst Politecn Leiria Leiria Portugal

ISBN: (纸本)9783642237157;9783642237164

Model checking is a fully automatic technique for checking concurrent software properties in which the states of a concurrent system are explored in an explicit or implicit way. The main drawback of this technique is the high memory consumption, which limits the size of the programs that can be checked. In the last years, some researchers have focused on the application of guided non-complete stochastic techniques to the search of the state space of such concurrent programs. In this paper, we compare five metaheuristic algorithms for this problem. The algorithms are Simulated Annealing, Ant Colony Optimization, Particle Swarm Optimization and two variants of Genetic Algorithm. To the best of our knowledge, it is the first time that Simulated Annealing has been applied to the problem. We use in the comparison a benchmark composed of 17 java concurrent programs. We also compare the results of these algorithms with the ones of deterministic algorithms.

关键词： Model checking java pathfinder simulated annealing particle swarm optimization ant colony optimization genetic algorithm

来源：评论

学校读者我要写书评

暂无评论

Modeling UASs for Role Fusion and Human Machine Interface Optimization

Modeling UASs for Role Fusion and Human Machine Interface Op...

引用

IEEE International Conference on Systems, Man, and Cybernetics (SMC)

作者： Gledhill, T. J. Mercer, Eric Goodrich, Michael A. Brigham Young Univ Dept Comp Sci Provo UT 84602 USA

ISBN: (纸本)9781479906529

Currently, a single Unmanned Aerial System (UAS) requires several humans managing different aspects of the problem. Human roles often include vehicle operators, payload experts, and mission managers [1-3]. As a step toward reducing the number of humans required, it is desirable to reduce operator workload through effective distributed control, augmented autonomy, and intelligent user interfaces. Reliably doing this requires various roles in the system to be modeled. These roles naturally include the roles of the humans, but they also include roles delegated to autonomy and software decision-making algorithms, meaning the GUI and the unmanned aerial vehicle. This paper presents a conceptual model which models the roles of complex systems as a collection of actors, running in parallel. Results from applying this model to the UAS-enabled Wilderness Search and Rescue (WiSAR) domain indicate (a) it is possible to model the entire WiSAR system at varying degrees of abstraction (b) that building and evaluating the model provides insight into the best practices of WiSAR teams and (c) a way to model human machine interactions that works directly with the java pathfinder model checker to detect errors.

关键词： model checking human machine interfaces java pathfinder Unmanned Aerial Systems Wilderness Search and Rescue

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Software Model Checking of UDP-based Distributed Applications 2

Software Model Checking of UDP-based Distributed Application...

引用

International Symposium on Computing and Networking CANDAR

作者： Sebih, Nazim Weitl, Franz Artho, Cyrille Hagiya, Masami Tanabe, Yoshinori Yamamoto, Mitsuharu Univ Tokyo Tokyo Japan Chiba Univ Chiba Japan AIST RISEC Amagasaki Hyogo Japan Natl Inst Informat Tokyo Japan

ISBN: (纸本)9781479941520

We extend exhaustive verification of networked applications to applications using the User Datagram Protocol (UDP). UDP maximizes performance by omitting flow control and connection handling. High-performance services often offer a UDP mode in which they handle connections internally for optimal throughput. However, because UDP is unreliable (packets are subject to loss, duplication, and reordering), verification of UDP-based applications becomes an issue. Even though unreliable behavior occurs only rarely during testing, it often appears in a production environment due to a larger number of concurrent network accesses. Our tool systematically tests UDP-based applications by producing packet loss, duplication, and reordering for each packet. It is built on top of net-iocache for the java pathfinder model checker. We have evaluated the performance of our tool in a multi-threaded client/server application and detected incorrectly handled packet duplicates in a file transfer client.

关键词： Software Model Checking java pathfinder Testing of Distributed Systems User Datagram Protocol Unreliable Network IO

来源：评论

学校读者我要写书评

暂无评论

Cardinality of UDP Transmission Outcomes 1st

Cardinality of UDP Transmission Outcomes

引用

1st International Symposium on Dependable Software Engineering - Theories, Tools and Applications (SETTA)

作者： Weitl, Franz Sebih, Nazim Artho, Cyrille Hagiya, Masami Tanabe, Yoshinori Yamagata, Yoriyuki Yamamoto, Mitsuharu Chiba Univ Chiba Japan AIST RISEC Amagasaki Hyogo Japan Univ Tokyo Tokyo Japan Tsurumi Univ Yokohama Kanagawa Japan

ISBN: (纸本)9783319259420;9783319259413

This paper examines the cost of testing network applications using the User Datagram Protocol (UDP). Such applications must deal with packet loss, duplication, and reordering. Ideally, a UDP application should be tested against all possible outcomes of unreliable UDP transmissions. Their number, however, grows at least exponentially in the number of transmitted packets. To estimate the cost of the exhaustive testing of UDP applications, we determine the number of UDP transmission outcomes analytically. Based on this combinatorial analysis, we derive a sound, complete, and optimal algorithm for generating outcomes of unreliable UDP transmissions. The algorithm is implemented in the net-iocache extension of the software model checker java pathfinder (JPF). Experimental results confirm the consistency of the implementation with the analytical results. In addition, we found that JPF's state matching reduces the explored state space significantly and ensures the practicability of the approach despite of its exponential complexity.

关键词： User datagram protocol Software model checking java pathfinder Combinatorial analysis

来源：评论

学校读者我要写书评

暂无评论

Simulation Testing and Model Checking: A Case Study Comparing these Approaches 6

Simulation Testing and Model Checking: A Case Study Comparin...

引用

6th International Workshop on Software Engineering for Resilient Systems (SERENE)

作者： Lipka, Richard Paska, Marek Potuzak, Tomas Univ West Bohemia NTIS Plzen 30614 Czech Republic Univ West Bohemia Fac Sci Appl Dept Comp Sci & Engn Plzen Czech Republic

ISBN: (纸本)9783319122410;9783319122403

One of the challenging problems in software development is the assuring of the correctness of the created software. During our previous research, we developed a framework for the simulation-based testing of software components SimCo that allows us to perform testing of component-based applications or its fragments. The SimCo was originally designed to perform the tests according to a given scenario in order to determine extra-functional properties of the components. However, it can be also used to test the correctness of the component behaviour. For this purpose, there are also other ways - the model checking tools, such as java pathfinder. We want to compare the strengths and weaknesses of the two approaches as represented by the SimCo and the java pathfinder. In this paper, the results of the comparison of these two testing methods on a case study using the implementation of the FTP protocol are discussed.

关键词： software component simulation testing model checking java pathfinder SimCo defect discovery

来源：评论

学校读者我要写书评

暂无评论

User-Friendly GUI in Software Model Checking

User-Friendly GUI in Software Model Checking

引用

IEEE International Conference on Systems, Man and Cybernetics

作者： Yokoyama, Shoichi Sato, Haruhiko Kurihara, Masahito Hokkaido Univ Grad Sch Informat Sci & Technol Sapporo Hokkaido Japan

ISBN: (纸本)9781424427932

Model Checking is an automatic technique for verifying finite-state concurrent systems such as communication protocols and sequential circuit designs. It has a number of advantages over traditional approaches to this problem that are based on simulation, testing, and deductive reasoning. Model checking tools are, however, not widely introduced into industry, and one of the reasons is that they are tricky and difficult to use for engineers. In this paper, we extend the functions of java pathfinder, a software model checker to verify executable java bytecode programs, and propose a graphical user interface with a high degree of usability. Our GUI depicts the state transition graphs of not only a whole program but also each thread as a result of verification. Users can get much information through the GUI, for example, the internal states of a program and the correspondence relation between the graphs, with interactive mouse operation. One of the key features of our GUI is a variable-value-based graph abstraction that allows users to focus upon an aspect they are interested in. Our GUI also has an intuitively easy-to-use interface for users to input linear temporal logic (LTL) formulae as a program specification based on the Specification Pattern System.

关键词： Model Checking GUI java pathfinder

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

全选清除本页清除全部题录导出标记到“检索档案”

共3页 << < 1 2 3 > >>

检索报告对象比较合并检索0

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

电话和邮箱必须正确填写，我们会与您联系确认。

联系人：

所在院系：

联系邮箱：

联系电话：

内蒙古自治区呼和浩特市赛罕区大学西街235号邮编: 010021

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：