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

Annual IEEE/ NASA Goddard Workshop on Software Engineering

作者： Huibiao Zhu Shengchao Qin Jifeng He Jonathan P. Bowen Software Engineering Institute East China Jiao Tong University China Department of Computer Science University of Durham UK Centre for Applied Formal Methods London South Bank University UK

Complex software systems typically involve features like time, concurrency and probability, where probabilistic computations play an increasing role. It is challenging to formalize languages comprising all these features. In this paper, we integrate probability, time and concurrency in one single model, where the concurrency feature is modelled using shared-variable based communication. The probability feature is represented by a probabilistic nondeterministic choice, probabilistic guarded choice and a probabilistic version of parallel composition. We formalize an operational semantics for such an integration. Based on this model we define a bisimulation relation, from which an observational equivalence between probabilistic programs is investigated and a collection of algebraic laws are explored. We also implement a prototype of the operational semantics to animate the execution of probabilistic programs

关键词： Concurrent computing Software engineering Software systems Helium Prototypes Animation Hardware design languages Command languages computer science Time sharing computer systems

来源：评论

学校读者我要写书评

暂无评论

Timed Testing with TorX

Timed Testing with TorX

引用

ITG FA 6.2 Workshop on Model-Based Testing, GI/ITG Workshop on Non-Functional Properties of Embedded Systems, 13th GI/ITG Conference Measuring, Modelling, and Evaluation of computer and Communications

作者： Henrik Bohnenkamp Axel Belinfante Software Modelling and Verification Group (Informatik 2) RWTH Aachen University D-52056 Germany Formal Methods and Tools Department of Computer Science University of Twente Postbus 217 NL-7500 AE Enschede The Netherlands

We describe an approach to on-the-fly real-time testing based on non-deterministic timed automata. The approach is based on standard computations on zone automata. We present algorithms for practical testing, as they ... 详细信息

关键词： Automata Testing Semantics Real time systems Cost accounting Atomic clocks

来源：评论

学校读者我要写书评

暂无评论

YMCA

引用

Electronic Notes in Theoretical computer science 2006年 162卷 107-112页

作者： Mario Bravetti Holger Hermanns Joost-Pieter Katoen Dipartimento di Scienze dell'Informazione Università di Bologna Mura Anteo Zamboni 7 I-40127 Bologna Italy Dependable Systems & Software Department of Computer Science Saarland University 66123 Saarbruecken Germany and University of Twente Formal Methods and Tools P.O. Box 217 7500 AE Enschede The Netherlands RWTH Aachen Software Modeling and Verification Ahornstrasse 55 D-52074 Aachen Germany

Markov chains are widely used to determine system performance and reliability characteristics. The vast majority of applications considers continuous-time Markov chains (CTMCs). This note motivates how concurrency theory can be extended (as opposed to twisted ) to CTMCs. We provide the core motivation for the algebraic setup of Interactive Markov Chains . Therefore, this note should have better been baptized YIMC.

关键词： Markov chain process algebra concurrency theory

来源：评论

学校读者我要写书评

暂无评论

The DILIGENT knowledge processes

引用

Journal of Knowledge Management 2005年第5期9卷 85-96页

作者： Vrandečić, Denny Pinto, Sofia Tempich, Christoph Sure, York University of Karlsruhe Institute of Applied Informatics and Formal Description Methods 76128 Karlsruhe Germany Department of Computer Science and Engineering Instituto Superior Tecnico Technical University of Lisbon Lisbon Portugal Institute of Applied Computer Science and Formal Description Methods University of Karlsruhe 76128 Karlsruhe Germany

Purpose - Aims to present the ontology engineering methodology DILIGENT, a methodology focussing on the evolution of ontologies instead of the initial design, thus recognizing that knowledge is a tangible and moving target. Design/methodology/approach - First describes the methodology as a whole, then detailing one of the five main steps of DILIGENT. The second part describes case studies, either already performed or planned, and what we learned (or expect to learn) from them. Findings - With the case studies it was discovered the strengths and weaknesses of DILIGENT. During the evolution of ontologies, arguments need to be exchanged about the suggested changes. Identifies those kind of arguments which work best for the discussion of ontology changes. Research implications - DILIGENT recognizes ontology engineering methodologies like OnToKnowledge or Methontology as proven useful for the initial design, but expands them with its strong focus on the user-centric further development of the ontology and the provided integration of automatic agents in the process of ontology evolution. Practical implications - With DILIGENT the experience distilled from a number of case studies and offers the knowledge manager a methodology to work in an ever-changing environment. Originality/value - DILIGENT is the first methodology to put focus not on the initial development of the ontology, but on the user and his usage of the ontology, and on the changes introduced by the user. We take the user's own view seriously and enable feedback towards the evolution of the ontology, stressing the ontology's role as a shared conceptualisation. © Emerald Group Publishing Limited.

关键词： computer applications Knowledge management systems Semantics User interfaces

来源：评论

学校读者我要写书评

暂无评论

Management of dynamic knowledge

引用

Journal of Knowledge Management 2005年第5期9卷 97-107页

作者： Haase, Peter Völker, Johanna Sure, York Knowledge Management Group Institute of Applied Computer Science and Formal Description Methods University of Karlsruhe 76128 Karlsruhe Germany Institute of AIFB University of Karlsruhe 76128 Karlsruhe Germany Institute of Applied Computer Sciences and Formal Description Methods University of Karlsruhe 76128 Karlsruhe Germany

Purpose - This paper presents a framework for ontology evolution tailored to Digital Libraries, which makes use of two different sources for change detection and propagation, the usage of ontologies by users and the changes of available data. Design/methodology/approach - After presenting the logical architecture of the evolution framework, we first illustrate how to deal with usage-driven changes, that is changes derived from the actual usage of ontologies. Second, we describe the generation of data-driven ontology changes based on the constant flow of documents coming into digital libraries. Findings - The proposed framework for ontology ontology evolution, which is currently applied and evaluated in the case studies, significantly reduces the costs of ontology updates and improves the quality of the ontology with respect to the user's requirements. Practical implications - The management of dynamic knowledge is crucial for many knowledge management applications. Our approach for usage-driven and data-driven change discovery not only assures the consistency of ontologies modeling dynamic knowledge, but also reduces the burden of manual ontology engineering. Originality/value - This paper presents the first approach towards a common framework for ontology evolution based on usage-driven and data-driven change discovery. © Emerald Group Publishing Limited.

关键词： Data handling Digital libraries Information retrieval Knowledge management

来源：评论

学校读者我要写书评

暂无评论

The formal verification of a reintegration protocol

The formal verification of a reintegration protocol

引用

5th ACM International Conference on Embedded Software, EMSOFT 2005

作者： Pike, Lee Johnson, Steven D. Formal Methods Group NASA Langley Research Center United States Department of Computer Science Indiana University Bloomington United States

ISBN: (纸本)1595930914

We report the first formal verification of a reintegration protocol for a safety-critical distributed embedded system. A reintegration protocol increases system survivability by allowing a transiently-faulty node to regain state. The protocol is verified in the Symbolic Analysis Laboratory (SAL), where bounded model-checking and decision procedures are used to verify infinite-state systems by k-induction. The protocol and its environment are modeled using a recently-developed explicit real-time model. Because k-induction has exponential complexity, we optimize this model to reduce the size of k necessary for the verification and to make k invariant to the number of nodes. A corollary of the verification is that a clique avoidance property is satisfied. Copyright 2005 ACM.

关键词： Network protocols

来源：评论

学校读者我要写书评

暂无评论

An overview of systemCdouble-struck F signdouble-struck L sign

An overview of systemCdouble-struck F signdouble-struck L si...

引用

2005 PhD Research in Microelectronics and Electronics Conference

作者： Man, K.L. Formal Methods Group Department of Mathematics and Computer Science Eindhoven University of Technology P.O.Box 513 5600 MB Eindhoven Netherlands

ISBN: (纸本)0780393457

This paper describes our on-going research. Recently, we developed an algebraic theory based on classical process algebra ACP, called SystemC double-struck F signdouble-struck L sign, for the specification and analysis of SystemC designs. The semantics of SystemC double-struck F signdouble-struck L sign is defined by means of deduction rules in a standard structured operational semantics style that associate a labelled transition transition system with a SystemC double-struck F signdouble-struck L sign process. In this paper, we first provide an overview of the current status of SystemC double-struck F signdouble-struck L sign and show some practical applications of SystemCdouble-struck F signdouble-struck L sign, as well as some key features and results of SystemC double-struck F signdouble-struck L sign. Then, we give an out-line for the latest developments of SystemC double-struck F signdouble-struck L sign and point out the direction for future work.

关键词： Systems engineering

来源：评论

学校读者我要写书评

暂无评论

formal communication semantics of SystemCdouble-struck F sign double-struck L sign

Formal communication semantics of SystemCdouble-struck F sig...

引用

DSD'2005: 8th Euromicro Conference on Digital System Design

作者： Man, K.L. Formal Methods Group Department of Mathematics and Computer Science Eindhoven University of Technology P.O.Box 513 5600 MB Eindhoven Netherlands

ISBN: (纸本)0769524338

In this paper, we define a formal communication semantics for SystemCdouble-struck F sign double-struck L sign that deals with concurrency and interaction. The communication semantics of SystemCdouble-struck F sign double-struck L sign is formally defined in a standard structured operational semantics (SOS) style. The correctness of the proposed communication semantics of SystemCdouble-struck F sign double-struck L sign is also validated. A case study (RPC protocol with refinement) is given to illustrate the use of the newly developed communication semantics of SystemCdouble-struck F sign double-struck L sign. © 2005 IEEE.

关键词： Systems analysis

来源：评论

学校读者我要写书评

暂无评论

SystemCdouble struck F sign double struck L sign: A formalism for hardware/software co-design

SystemCdouble struck F sign double struck L sign: A formalis...

引用

2005 European Conference on Circuit Theory and Design

作者： Man, K.L. Formal Methods Group Department of Mathematics and Computer Science Eindhoven University of Technology P.O.Box 513 5600 MB Eindhoven Netherlands

ISBN: (纸本)0780390660

SystemCdouble struck F sign double struck L sign is a formal language for hardware/software co-design. Principally, SystemCdouble struck F sign double struck L sign;is the formalization of SystemC based on classical process algebra ACP. The language Is aimed to give formal specification of SystemC designs and perform formal analysis of SystemC processes. This paper, designed for the first-time user of SystemCdouble struck F sign double struck L sign;, guides the reader through modeling, analyzing and verifying designs using SystemCdouble struck F sign double struck L sign;. This paper Illustrates the use of SystemCdouble struck F sign double struck L sign;with two case studies taken from literature.

关键词： computer architecture

来源：评论

学校读者我要写书评

暂无评论

Reachability analysis of synchronized PA systems

Reachability analysis of synchronized PA systems

引用

Proceedings of the 6th International Workshop on Verification of Infinite-State Systems (INFINITY 2004)

作者： Bouajjani, Ahmed Esparza, Javier Touili, Tayssir Liafa University of Paris 7 2 place Jussieu 75251 Paris Cedex 5 France Institute for Formal Methods in Computer Science University of Stuttgart Universitätstr. 38 70569 Stuttgart Germany

We present a generic approach for the analysis of concurrent programs with (unbounded) dynamic creation of threads and recursive procedure calls. We define a model for such programs based on a set of term rewrite rules where terms represent control configurations. The reachability problem for this model is undecidable. Therefore, we propose a method for analyzing such models based on computing abstractions of their sets of computation paths. Our approach allows to compute such abstractions as least solutions of a system of (path language) constraints. More precisely, given a program and two regular sets of configurations (process terms) T and T′, we provide (1) a construction of a system of constraints which characterizes the set of computation paths leading from T to T′, and (2) a generic framework, based on abstract interpretation, allowing to solve this system in various abstract domains leading to abstract analysis with different precision and cost. © 2005 Elsevier B.V. All rights reserved.

关键词： Synchronization

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：