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

25th Australasian Conference on Information Systems, ACIS 2014

作者： Gruner, Stefan Kroeze, Jan Research Group for System Specifications and Formal Methods Department of Computer Science Universiteit Van Pretoria South Africa

In this paper we argue that the so-called 'positivism'-versus-'interpretivism' conflict raised by some constructivist, postmodernist, relativist philosophers and methodologists in information systems research is merely a pseudo problem which has no basis in reality. This pseudo problem of so-called 'positivism' versus 'interpretivism' only distracts from the genuine problem of the information systems discipline, namely the design and construction of reliable devices from reasonable specifications, for well-defined purposes, on the basis of scientifically acceptable principles. In contrast to those relativist 'philosophies' we show that information systems research actually belongs to the domain of engineering which already has its time-tested methodology and epistemology, including a trinity of scientific-nomothetic, hermeneutic-idiographic, as well as pragmatic-normative elements. By accepting fact that information systems research is a specific instance of engineering research, which also includes (and has always included) the un-quantifiable 'human dimension', a number of fruitless debates can be terminated for the sake of genuine progress in information systems' theory, design and *** Gruner and Jan Kroeze © 2014.

关键词： Information use

来源：评论

学校读者我要写书评

暂无评论

A Tutorial on Interactive Markov chains

Lecture Notes in Computer Science (including subseries Lectu...

引用

Lecture Notes in computer science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2014年 8453卷 26-66页

作者： Arnold, Florian Gebler, Daniel Guck, Dennis Hatefi, Hassan Formal Methods and Tools Group Department of Computer Science University of Twente P.O. Box 217 Enschede7500 AE Netherlands Department of Computer Science VU University Amsterdam De Boelelaan 1081a AmsterdamNL-1081 HV Netherlands Department of Computer Science Saarland University Saarbrücken66123 Germany

Interactive Markov chains (IMCs) constitute a powerful stochastic model that extends both continuous-time Markov chains and labelled transition systems. IMCs enable a wide range of modelling and analysis techniques and serve as a semantic model for many industrial and scientific formalisms, such as AADL, GSPNs and many more. Applications cover various engineering contexts ranging from industrial systemon- chip manufacturing to satellite designs. We present a survey of the state-of-the-art in modelling and analysis of IMCs. We cover a set of techniques that can be utilised for compositional modelling, state space generation and reduction, and model checking. The significance of the presented material and corresponding tools is highlighted through multiple case studies. © 2014 Springer-Verlag Berlin Heidelberg.

关键词： Model checking

来源：评论

学校读者我要写书评

暂无评论

A tutorial on interactive Markov chains

A tutorial on interactive Markov chains

引用

International Autumn School on Stochastic Model Checking : Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems, ROCKS 2012

作者： Arnold, Florian Gebler, Daniel Guck, Dennis Hatefi, Hassan Formal Methods & Tools Group Department of Computer Science University of Twente P.O. Box 217 Enschede7500 AE Netherlands Department of Computer Science VU University Amsterdam De Boelelaan 1081a AmsterdamNL-1081 HV Netherlands Department of Computer Science Saarland University Saarbrücken66123 Germany

ISBN: (纸本)9783662454886

Interactive Markov chains (IMCs) constitute a powerful sto- chastic model that extends both continuous-time Markov chains and labelled transition systems. IMCs enable a wide range of modelling and analysis techniques and serve as a semantic model for many industrial and scientific formalisms, such as AADL, GSPNs and many more. Applications cover various engineering contexts ranging from industrial system-on-chip manufacturing to satellite designs. We present a survey of the state-of-the-art in modelling and analysis of IMCs. We cover a set of techniques that can be utilised for compositional modelling, state space generation and reduction, and model checking. The significance of the presented material and corresponding tools is highlighted through multiple case studies. © 2014, Springer-Verlag Berlin Heidelberg.

关键词： System-on-chip

来源：评论

学校读者我要写书评

暂无评论

Time-dependent analysis of attacks

Time-dependent analysis of attacks

引用

3rd International Conference on Principles of Security and Trust, POST 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014

作者： Arnold, Florian Hermanns, Holger Pulungan, Reza Stoelinga, Mariëlle Formal Methods and Tools Group Department of Computer Science University of Twente P.O. Box 217 7500 AE Enschede Netherlands Dependable Systems and Software Saarland University 66123 Saarbrücken Germany Jurusan Ilmu Komputer Dan Elektronika Universitas Gadjah Mada Indonesia

ISBN: (纸本)9783642547911

The success of a security attack crucially depends on time: the more time available to the attacker, the higher the probability of a successful attack;when given enough time, any system can be compromised. Insight in time-dependent behaviors of attacks and the evolution of the attacker's success as time progresses is therefore a key for effective countermeasures in securing systems. This paper presents an efficient technique to analyze attack times for an extension of the prominent formalism of attack trees. If each basic attack step, i.e., each leaf in an attack tree, is annotated with a probability distribution of the time needed for this step to be successful, we show how this information can be propagated to an analysis of the entire tree. In this way, we obtain the probability distribution for the entire system to be attacked successfully as time progresses. For our approach to be effective, we take great care to always work with the best possible compression of the representations of the probability distributions arising. This is achieved by an elegant calculus of acyclic phase type distributions, together with an effective compositional compression technique. We demonstrate the effectiveness of this approach on three case studies, exhibiting orders of magnitude of compression. © 2014 Springer-Verlag.

关键词： Probability distributions

来源：评论

学校读者我要写书评

暂无评论

Multi-core emptiness checking of timed Büchi automata using inclusion abstraction

引用

25th International Conference on computer Aided Verification, CAV 2013

作者： Laarman, Alfons Olesen, Mads Chr. Dalsgaard, Andreas Engelbredt Larsen, Kim Guldstrand Van De Pol, Jaco Formal Methods and Tools University of Twente Netherlands Department of Computer Science Aalborg University Denmark

ISBN: (纸本)9783642397981

This paper contributes to the multi-core model checking of timed automata (TA) with respect to liveness properties, by investigating checking of TA Büchi emptiness under the very coarse inclusion abstraction or zone subsumption, an open problem in this field. We show that in general Büchi emptiness is not preserved under this abstraction, but some other structural properties are preserved. Based on those, we propose a variation of the classical nested depth-first search (ndfs) algorithm that exploits subsumption. In addition, we extend the multi-core cndfs algorithm with subsumption, providing the first parallel LTL model checking algorithm for timed automata. The algorithms are implemented in LTSmin, and experimental evaluations show the effectiveness and scalability of both contributions: subsumption halves the number of states in the real-world FDDI case study, and the multi-core algorithm yields speedups of up to 40 using 48 cores. © 2013 Springer-Verlag.

关键词： Model checking

来源：评论

学校读者我要写书评

暂无评论

On-the-fly confluence detection for statistical model checking

引用

5th International Symposium on NASA formal methods, NFM 2013

作者： Hartmanns, Arnd Timmer, Mark Saarland University - Computer Science Saarbrücken Germany Formal Methods and Tools University of Twente Netherlands

ISBN: (纸本)9783642380877

Statistical model checking is an analysis method that circumvents the state space explosion problem in model-based verification by combining probabilistic simulation with statistical methods that provide clear error bounds. As a simulation-based technique, it can only provide sound results if the underlying model is a stochastic process. In verification, however, models are usually variations of nondeterministic transition systems. The notion of confluence allows the reduction of such transition systems in classical model checking by removing spurious nondeterministic choices. In this paper, we show that confluence can be adapted to detect and discard such choices on-the-fly during simulation, thus extending the applicability of statistical model checking to a subclass of Markov decision processes. In contrast to previous approaches that use partial order reduction, the confluence-based technique can handle additional kinds of nondeterminism. In particular, it is not restricted to interleavings. We evaluate our approach, which is implemented as part of the modes simulator for the Modest modelling language, on a set of examples that highlight its strengths and limitations and show the improvements compared to the partial order-based method. © 2013 Springer-Verlag.

关键词： Model checking

来源：评论

学校读者我要写书评

暂无评论

Complex Systems Design & Management: Proceedings of the Fourth International Conference on Complex Systems Design & Management CSD&M 2013

引用

2013年

作者： Marc Aiguier Frédéric Boulanger Daniel Krob Clotilde Marchal

ISBN: (纸本)9783319028118

This book contains all refereed papers that were accepted to the fourth edition of the Complex Systems Design & Management (CSD&M 2013) international conference which took place in Paris (France) from December 4-6, *** proceedings cover the most recent trends in the emerging field of complex systems sciences & practices from an industrial and academic perspective, including the main industrial domains (transport, defense & security, electronics, energy & environment, e-services), scientific & technical topics (systems fundamentals, systems architecture & engineering, systems metrics & quality, systemic tools) and system types (transportation systems, embedded systems, software & information systems, systems of systems, artificial ecosystems).The CSD&M 2013 conference is organized under the guidance of the CESAMES non-profit organization.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Presenting distributive laws

Presenting distributive laws

引用

5th International Conference on Algebra and Coalgebra in computer science, CALCO 2013

作者： Bonsangue, Marcello M. Hansen, Helle Hvid Kurz, Alexander Rot, Jurriaan LIACS - Leiden University Netherlands ICIS/IS - Radboud University Nijmegen Netherlands Formal Methods - Centrum Wiskunde and Informatica Amsterdam Netherlands Dep. of Computer Science University of Leicester United Kingdom

ISBN: (纸本)9783642402050

Distributive laws of a monad over a functor F are categorical tools for specifying algebra-coalgebra interaction. They proved to be important for solving systems of corecursive equations, for the specification of well-behaved structural operational semantics and, more recently, also for enhancements of the bisimulation proof method. If is a free monad, then such distributive laws correspond to simple natural transformations. However, when is not free it can be rather difficult to prove the defining axioms of a distributive law. In this paper we describe how to obtain a distributive law for a monad with an equational presentation from a distributive law for the underlying free monad. We apply this result to show the equivalence between two different representations of context-free languages. © 2013 Springer-Verlag Berlin Heidelberg.

关键词： Context free languages

来源：评论

学校读者我要写书评

暂无评论

Unified Execution of Service Compositions (Short Paper)

Unified Execution of Service Compositions (Short Paper)

引用

IEEE International Conference on Service-Oriented Computing and Applications (SOCA)

作者： Katharina Görlach Frank Leymann Volker Claus Institute of Architecture of Application Systems University of Stuttgart Institute for Formal Methods in Computer Science University of Stuttgart

This paper discusses the unification of service composition based on formal specifications. The approach aims for a unified execution of service compositions that can be modeled by various specification languages covering different modeling paradigms. The unification of service composition models is realized based on formal grammars whereas the unification of service composition execution is realized based on formal queued automata. The approach introduces a classification of context-sensitive grammars for determining an optimized automaton class for the execution of service compositions. Finally, a prototype providing transformations of various modeling languages to formal grammars as well as the grammar-based execution of service compositions is presented.

关键词： Grammar Automata Context Unified modeling language Production Runtime Engines

来源：评论

学校读者我要写书评

暂无评论

Connected dominating sets on dynamic geometric graphs

Connected dominating sets on dynamic geometric graphs

引用

作者： Guibas, Leonidas Milosavljević, Nikola Motskin, Arik Computer Science Department Gates Building Stanford University Stanford CA 94305 United States Institute of Formal Methods in Computer Science University of Stuttgart Universitätsstr. 38 D-70569 Stuttgart Germany Google Inc. 1600 Amphitheatre Parkway Mountain View CA 94043 United States

We propose algorithms for efficiently maintaining a constant-approximate minimum connected dominating set (MCDS) of a geometric graph under node insertions and deletions, and under node mobility. Assuming that two nodes are adjacent in the graph if and only if they are within a fixed geometric distance, we show that an O(1)-approximate MCDS of a graph in Rd with n nodes can be maintained in O(log2dn) time per node insertion or deletion. We also show that Ω(n) time per operation is necessary to maintain exact MCDS. This lower bound holds even for d=1, even for randomized algorithms, and even when running time is amortized over a sequence of insertions/deletions, or over continuous motion. The crucial fact is that a single operation may affect the entire exact solution, while an approximate solution is affected only in a small neighborhood of the node that was inserted or deleted. In the approximate case, we show how to compute these local changes by a few range searching queries and a few bichromatic closest pair queries. © 2012 Elsevier B.V. All rights reserved.

关键词： Geometry

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：