基于Verics的组合Web服务有界模型检测

传统的模型检测技术无法描述系统的认知逻辑特性,而在分布式系统领域,系统和协议的规范适合用多智能体时态认知逻辑来描述.组合Web服务是典型的分布式系统.为了保证组合Web服务运行的正确性,把组合Web服务看成多智能体系统,将其建模成一组相互通信的时间自动机.采用时态认知逻辑模型检测工具Verics对该组合Web服务的可用性、可靠性和时效性的时态认知逻辑特性进行检测.本文以旅游预订系统组合Web服务为例,阐述了上述过程.     

Fully Symbolic Unbounded Model Checking for Alternating-time Temporal Logic<Superscript>1</Superscript>

Alternating-time Temporal Logic (ATL) is typically applied for specifying properties of multi-agent systems modelled by game-like structures. This paper deals with verification of ATL by means of a fully symbolic model checking. Unbounded model checking (a SAT-based technique) is applied for the first time to verification of AT. Several examples are given in order to present an application of the technique.The authors acknowledge support from the two Polish grants: W/IMF/2/04 and 3 T11C 011 28.     

Verifying concurrent probabilistic systems using probabilistic-epistemic logic specifications

In this paper, we address the problem of verifying probabilistic and epistemic properties in concurrent probabilistic systems expressed in PCTLK. PCTLK is an extension of the Probabilistic Computation Tree Logic (PCTL) augmented with Knowledge (K). In fact, PCTLK enjoys two epistemic modalities K_i for knowledge and \(Pr_{\triangledown b}K_{i}\) for probabilistic knowledge. The approach presented for verifying PCTLK specifications in such concurrent systems is based on a transformation technique. More precisely, we convert PCTLK model checking into the problem of model checking Probabilistic Branching Time Logic (PBTL), which enjoys path quantifiers in the range of adversaries. We then prove that model checking a formula of PCTLK in concurrent probabilistic programs is PSPACE-complete. Furthermore, we represent models associated with PCTLK logic symbolically with Multi-Terminal Binary Decision Diagrams (MTBDDs), which are supported by the probabilistic model checker PRISM. Finally, an application, namely the NetBill online shopping payment protocol, and an example about synchronization illustrated through the dining philosophers problem are implemented with the MTBDD engine of this model checker to verify probabilistic epistemic properties and evaluate the practical complexity of this verification.     

Agent systems verification : systematic literature review and mapping

Agent systems are distributed systems consist of agents that autonomously interact to each other in an environment to perform tasks and achieve goals. Performing verification is important to ensure correctness of agent properties and to detect faults. The objective of this review is to identify research gap and future research direction of agent systems verification. In this study, the surveys of existing techniques for checking agent properties and detecting faults during design, development and runtime phases of agent system life-cycle are presented. Search terms with relevant keywords were used to identify primary studies that relate to the topic of discussion. Next, the studies were classified based on the used techniques and the addressed properties. 231 primary studies were identified during the search process. From these studies, 49% were implemented for verification of agent systems during design, 27% during development and 25% during runtime. Model checking or model-based verification techniques are the highest proposed techniques (44%) followed by the testing and debugging during development (17%). The properties that are largely addressed by the selected studies are temporal properties (19%) and epistemic properties (9%). At the end of the review, the research gap and the future research direction are presented.     

Scientific Theories of Computational Systems in Model Checking

Model checking, a prominent formal method used to predict and explain the behaviour of software and hardware systems, is examined on the basis of reflective work in the philosophy of science concerning the ontology of scientific theories and model-based reasoning. The empirical theories of computational systems that model checking techniques enable one to build are identified, in the light of the semantic conception of scientific theories, with families of models that are interconnected by simulation relations. And the mappings between these scientific theories and computational systems in their scope are analyzed in terms of suitable specializations of the notions of model of experiment and model of data. Furthermore, the extensively mechanized character of model-based reasoning in model checking is highlighted by a comparison with proof procedures adopted by other formal methods in computer science. Finally, potential epistemic benefits flowing from the application of model checking in other areas of scientific inquiry are emphasized in the context of computer simulation studies of biological information processing.     

Compositional encoding for bounded model checking

Verification techniques like SAT-based bounded model checking have been successfully applied to a variety of system models. Applying bounded model checking to compositional process algebras is, however, a highly non-trivial task. One challenge is that the number of system states for process algebra models is not statically known, whereas exploring the full state space is computationally expensive. This paper presents a compositional encoding of hierarchical processes as SAT problems and then applies state-of-the-art SAT solvers for bounded model checking. The encoding avoids exploring the full state space for complex systems so as to deal with state space explosion. We developed an automated analyzer which combines complementing model checking techniques (i.e., bounded model checking and explicit onthe-fly model checking) to validate system models against event-based temporal properties. The experiment results show the analyzer handles large systems.     

时态认知逻辑CTL＊K的符号化模型检查算法

时序认知逻辑是由时序逻辑和认知逻辑组合而成的逻辑,主要应用于多主体系统的规范定义.大多数时序认知逻辑是基于CTL的,表达能力有限.并且已知的一些模型检查算法存在内存不足和状态爆炸等问题.讨论了基于CTL*的时态认知逻辑cTL*K的语法、语义和模型,它能够在表达力很强的时态逻辑CTL*基础上描述智能体的知识、目标等意向特征.并给出了CTL*K的模型检查算法,其核心思想就是将CTL*K公式的检查问题转化为CTL*公式的模型检查问题,可以使检查的系统规模得以大幅度提高.并且将算法编码后容易集成到NuSMV模型检查器.     

Stochastic game logic

Stochastic game logic (SGL) is a new temporal logic for multi-agent systems modeled by turn-based multi-player games with discrete transition probabilities. It combines features of alternating-time temporal logic (ATL), probabilistic computation tree logic and extended temporal logic. SGL contains an ATL-like modality to specify the individual cooperation and reaction facilities of agents in the multi-player game to enforce a certain winning objective. While the standard ATL modality states the existence of a strategy for a certain coalition of agents without restricting the range of strategies for the semantics of inner SGL formulae, we deal with a more general modality. It also requires the existence of a strategy for some coalition, but imposes some kind of strategy binding to inner SGL formulae. This paper presents the syntax and semantics of SGL and discusses its model checking problem for different types of strategies. The model checking problem of SGL turns out to be undecidable when dealing with the full class of history-dependent strategies. We show that the SGL model checking problem for memoryless deterministic strategies as well as the model checking problem of the qualitative fragment of SGL for memoryless randomized strategies is PSPACE-complete, and we establish a close link between natural syntactic fragments of SGL and the polynomial hierarchy. Further, we give a reduction from the SGL model checking problem under memoryless randomized strategies into the Tarski algebra which proves the problem to be in EXPSPACE.     

一种求解认知难题的模型检测方法

用公告逻辑建模并求解和与积认知难题.提出一种动态认知模型,将环境认知模型与公告导致的认知模型线性组合,从而在时态认知逻辑模型检测技术中扩展支持公告逻辑的建模与验证.该模型检测方法不仅可以用于搜索认知难题的所有解,而且可以验证相关的时态认知性质,这一特性是当前认知逻辑模型检测工具MCK、MCMAS和DEMO不能完全支持的.作者采用OBDD开发了相关的符号化模型检测工具MCTK并对和与积难题进行建模和验证,实验结果说明了文中方法的正确性和高效性.     

Compositional analysis for verification of parameterized systems

Many safety-critical systems that have been considered by the verification community are parameterized by the number of concurrent components in the system, and hence describe an infinite family of systems. Traditional model checking techniques can only be used to verify specific instances of this family. In this paper, we present a technique based on compositional model checking and program analysis for automatic verification of infinite families of systems. The technique views a parameterized system as an expression in a process algebra (CCS) and interprets this expression over a domain of formulas (modal mu-calculus), considering a process as a property transformer. The transformers are constructed using partial model checking techniques. At its core, our technique solves the verification problem by finding the limit of a chain of formulas. We present a widening operation to find such a limit for properties expressible in a subset of modal mu-calculus. We describe the verification of a number of parameterized systems using our technique to demonstrate its utility.     

The role of model checking in software engineering

Model checking is a formal verification technique. It takes an exhaustively strategy to check hardware circuits and network protocols against desired properties. Having been developed for more than three decades, model checking is now playing an important role in software engineering for verifying rather complicated software artifacts.This paper surveys the role of model checking in software engineering. In particular, we searched for the related literatures published at reputed conferences, symposiums, workshops, and journals, and took a survey of (1) various model checking techniques that can be adapted to software development and their implementations, and (2) the use of model checking at different stages of a software development life cycle. We observed that model checking is useful for software debugging, constraint solving, and malware detection, and it can help verify different types of software systems, such as object- and aspect-oriented systems, service-oriented applications, web-based applications, and GUI applications including safety- and mission-critical systems.The survey is expected to help human engineers understand the role of model checking in software engineering, and as well decide which model checking technique(s) and/or tool(s) are applicable for developing, analyzing and verifying a practical software system. For researchers, the survey also points out how model checking has been adapted to their research topics on software engineering and its challenges.     

Bisimulation Minimization and Symbolic Model Checking

State space minimization techniques are crucial for combating state explosion. A variety of explicit-state verification tools use bisimulation minimization to check equivalence between systems, to minimize components before composition, or to reduce a state space prior to model checking. Experimental results on bisimulation minimization in symbolic model checking contexts, however, are mixed. This paper explores bisimulation minimization as an optimization in symbolic model checking of invariance properties. We consider three bisimulation minimization algorithms. From each, we produce a BDD-based model checker for invariant properties and compare this model checker to a conventional one based on backwards reachability. Our comparisons, both theoretical and experimental, suggest that bisimulation minimization is not viable in the context of invariance verification, because performing the minimization requires as many, if not more, computational resources as model checking the unminimized system through backwards reachability.     

可能性测度下的CTL符号化模型检测

随着系统复杂性的增加,系统中的不确定信息亟待处理,状态爆炸问题也越来越严峻,现有的模型检测技术已不能完全适用于复杂系统的验证。 对可能性测度下CTL符号化模型检测进行了研究。首先用多终端二值决策图和布尔公式分别描述系统模型和待验证性质,然后再对系统模型进行归一化和简化,最后利用不动点计算完成系统验证。该研究是对可能性测度下的模型检测技术和符号化模型检测技术的整合,不但能处理系统的不确定信息,而且保持了符号化模型检测对计算时空要求低的优点,对于复杂系统模型检测具有重要意义。     

Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs

Explicit-state model checking tools often incorporate partial-order reductions to reduce the number of system states explored (and thus the time and memory required) for verification. As model checking techniques are scaled up to software systems, it is important to develop and assess partial-order reduction strategies that are effective for addressing the complex structures found in software and for reducing the tremendous cost of model checking software systems. In this paper, we consider a number of reduction strategies for model checking concurrent object-oriented software. We investigate a range of techniques that have been proposed in the literature, improve on those in several ways, and develop five novel reduction techniques that advance the state of the art in partial-order reduction for concurrent object-oriented systems. These reduction strategies are based on (a) detecting heap objects that are thread-local (i.e., can be accessed by a single thread) and (b) exploiting information about patterns of lock-acquisition and release in a program (building on previous work). We present empirical results that demonstrate upwards of a hundred fold reduction in both space and time over existing approaches to model checking concurrent Java programs. In addition to validating their effectiveness, we prove that the reductions preserve LTL_?X properties and describe an implementation architecture that allows them to be easily incorporated into existing explicit-state software model checkers.     

Model-based verification of quantitative non-functional properties for software product lines

Evaluating quality attributes of a design model in the early stages of development can significantly reduce the cost and risks of developing a low quality product. To make this possible, software designers should be able to predict quality attributes by reasoning on a model of the system under development. Although there exists a variety of quality-driven analysis techniques for software systems, only a few work address software product lines. This paper describes how probabilistic model checking techniques and tools can be used to verify non-functional properties of different configurations of a software product line. We propose a model-based approach that enables software engineers to assess their design solutions for software product lines in the early stages of development. Furthermore, we discuss how the analysis time can be surprisingly reduced by applying parametric model checking instead of classic model checking. The results show that the parametric approach is able to substantially alleviate the verification time and effort required to analyze non-functional properties of software product lines.     

A classification and comparison of model checking software architecture techniques

Software architecture specifications are used for many different purposes, such as documenting architectural decisions, predicting architectural qualities before the system is implemented, and guiding the design and coding process. In these contexts, assessing the architectural model as early as possible becomes a relevant challenge. Various analysis techniques have been proposed for testing, model checking, and evaluating performance based on architectural models. Among them, model checking is an exhaustive and automatic verification technique, used to verify whether an architectural specification conforms to expected properties. While model checking is being extensively applied to software architectures, little work has been done to comprehensively enumerate and classify these different techniques.The goal of this paper is to investigate the state-of-the-art in model checking software architectures. For this purpose, we first define the main activities in a model checking software architecture process. Then, we define a classification and comparison framework and compare model checking software architecture techniques according to it.     

Game-based verification of contract signing protocols with minimal messages

A multi-party contract signing (MPCS) protocol is used for a group of signers to sign a digital contract over a network. We analyse the protocols of Mauw, Radomirović and Torabi Dashti (MRT), using the finite-state model checker Mocha. Mocha allows for the specification of properties in alternating-time temporal logic (ATL) with game semantics, and the model checking problem for ATL requires the computation of winning strategies. This gives us an intuitive interpretation of the verification problem of crucial properties of MPCS protocols. MRT protocols can be generated from minimal message sequences, depending on the number of signers. We discover an attack on fairness in a published MRT protocol with three signers and a general attack on abuse-freeness for all MRT protocols. For both attacks, we present solutions. The abuse-freeness attack leads us to a revision of the methodology to construct an MRT protocol. Following this revised methodology, we design a number of MRT protocols using minimal message sequences for three and four signers, all of whom have been successfully model checked in Mocha.     

Abstraction for model checking multi-agent systems

Model checking multi-agent systems (MAS) always suffers from the state explosion problem. In this paper we focus on an abstraction technique which is one of the major methods for overcoming this problem. For a multi-agent system, we present a novel abstraction procedure which reduces the state space by collapsing the global states in the system. The abstraction is automatically computed according to the property to be verified. The resulting abstract system simulates the concrete system, while the universal temporal epistemic properties are preserved. Our abstraction is an overapproximation. If some universal temporal epistemic property is not satisfied, then we need to identify spurious counterexamples. We further show how to reduce complex counterexamples to simple structures, i.e., paths and loops, such that the counterexamples can be checked and the abstraction can be refined efficiently. Finally, we illustrate the abstraction technique with a card game.