信息物理融合系统控制软件的统计模型检验

信息物理融合系统常采用嵌入式实时多任务系统作为其控制软件,这类软件的并发和非确定性给验证带来了困难.提出了一种利用统计模型检验技术分析多任务系统的功能正确性的方法.该方法构造的时间自动机模型以模块化的方式描述了实时多任务系统中的主要成分,包括实时操作系统、周期性任务、偶发任务、共享资源以及物理环境,能够展现多任务系统的细粒度的运行过程及其对物理环境的实时响应.应用该方法分析了玉兔号月球车控制软件的一个早期版本,发现了系统运行中出现的一个特殊错误,识别了实际系统出现错误的条件,再现了出现错误的场景.     

Partial model checking of modal equations: A survey

Partial model checking is a technique for verifying concurrent systems. It gradually reduces the verification problem to the final answer by removing concurrent components one-by-one, transforming and minimizing the specifications as it proceeds. This paper gives a survey of the theory behind partial model checking and the results obtained with it.     

一种自动的形式化验证技术-模型检测

模型检测是针对有限状态系统行为的逻辑性质的一种自动验证技术,已有许多工业应用.其主要缺陷是空间爆炸问题.本文通过一简单实例介绍其基本思想、检测步骤和相关理论,给出一些处理状态空间爆炸问题的优化技术,并与其它验证方法进行了比较,最后简单介绍了软件模型检测的新进展.     

State-based model checking of event-driven system requirements

It is demonstrated how model checking can be used to verify safety properties for event-driven systems. SCR tabular requirements describe required system behavior in a format that is intuitive, easy to read, and scalable to large systems (e.g. the software requirements for the A-7 military aircraft). Model checking of temporal logics has been established as a sound technique for verifying properties of hardware systems. An automated technique for formalizing the semiformal SCR requirements and for transforming the resultant formal specification onto a finite structure that a model checker can analyze has been developed. This technique was effective in uncovering violations of system invariants in both an automobile cruise control system and a water-level monitoring system     

具有多值决策过程的广义可能性计算树逻辑模型检测

模型检测是一种自动验证软硬件系统行为的有效技术。为了对包含非确定性信息、不一致信息的并发系统进行形式化验证,在可能性理论、多值逻辑的基础上,研究了具有多值决策过程的广义可能性多值计算树逻辑模型检测算法,及其在检验非确定性系统中的具体应用。首先构造了多值决策过程作为系统模型,用多值计算树逻辑描述系统属性。然后给出具有多值决策过程的广义可能性多值计算树逻辑的模型检测算法,该算法将模型检测的具体问题转换为多项式时间内的模糊矩阵运算。最后就包含非确定性选择的多值系统的模型检测问题,给出一个具体的应用实例。     

基于抽象-验证-细化范例的软件模型检测

如何保证软件系统的正确性和可靠性是当前软件开发面临的主要问题之一。模型检测作为一种重要的自动化验证技术在软件的分析与验证中正取得越来越多的成功。本文以微软的SLAM和加州大学伯克利分校的BLAST为例综述性地介绍了基于抽象-验证-细化范例的软件模型检测。     

面向复杂随机系统的启发式统计模型检测方法 *

统计模型检测是一种高效的验证技术,常用于复杂的随机系统验证,如分布式算法等。而在超长路径上对性质进行验证时,其验证效率会急剧降低。为解决这个问题,这里提出一种启发式的统计模型检测算法。在对路径进行验证时,我们会查找帮助剪枝的最短前缀。并在后续抽样时,利用前缀信息直接判定路径是否满足给定性质,避免进入费时的路径验证阶段。在与PRISM的比较中,它的路径验证次数相对更少且平均抽样路径长度更短。因此使统计模型检测技术可应用于超长路径上的性质验证。     

From NuSMV to SPIN: Experiences with model checking flight guidance systems

Model checking has become a promising technique for verifying software and hardware designs; it has been routinely used in hardware verification, and a number of case studies and industrial applications show its effectiveness in software verification as well. Nevertheless, most existing model checkers are specialized for limited aspects of a system, where each of them requires a certain level of expertise to use the tool in the right domain in the right way. Hardly any guideline is available on choosing the right model checker for a particular problem domain, which makes adopting the technique difficult in practice, especially for verifying software with high complexity. In this work, we investigate the relative pitfalls and benefits of using the explicit model checker Spin on commercial Flight Guidance Systems (FGSs) at Rockwell-Collins, based on the author's prior experience with the use of the symbolic model checker NuSMV on the same systems. This has been a question from the beginning of the project with Rockwell-Collins. The challenge includes the efficient use of Spin for the complex synchronous mode logic with a large number of state variables, where Spin is known to be not particulary efficient. We present the way the Spin model is optimized to avoid the state space explosion problem and discuss the implication of the result. We hope our experience can be a useful 21 reference for the future use of model checking in a similar domain.     

Model checking communicative agent-based systems

Model checking is a formal technique used to verify communication protocols against given properties. In this paper, we propose a new model checking algorithm aims at verifying systems designed as a set of autonomous interacting agents. These software agents are equipped with knowledge and beliefs and interact with each other according to protocols governed by a set of logical rules. We present a tableauased version of this algorithm and provide the soundness, completeness, termination and complexity results. A case study about an agent-based negotiation protocol and its implementation are also described.     

软件模型检测中的抽象

软件模型检测对保证软件的正确性和可靠性具有十分重要的意义，而抽象是减轻模型检测中状态爆炸问题最重要的技术之一。本文综述当前广泛应用于软件模型检测中的抽象技术，介绍了该领域的进展及研究方向。     

Detecting logic errors in discrete-event simulation: reverse engineering through event graphs

Several inherent constraints remain in the model development process, even though modern enhancements to simulation environments have provided tools for code generation, debugging, and tracing. To develop a simulation model, the simulation analyst still needs to have expertise in a number of different fields, e.g., probability, statistics, design of experiments, modeling, systems engineering, software engineering, and computer programming. Although several simulation packages implement syntactic-checks and semantic-consistency-checks, typically, the simulation analyst needs to possess output-analysis-knowledge specifically aimed at verifying and checking the simulation code.Reverse engineering a graphical model, e.g., an event graph, from general purpose simulation code demonstrates an enhancement to the model development process. A reverse engineering step allows an analyst to check, both, the static and dynamic properties of the coded simulation model. Even though the reverse engineering produces an event-oriented view, the enhanced model development process provides a systematic approach for conversion from other world views. Overall, this enhanced process provides a framework which yields better analysis techniques.Better diagnostic assistance is achieved when viewing a combination of static and dynamic properties of the simulation code. Now, the analyst is able to find logical/execution errors, e.g., errors related to resource deadlocks, before running simulation experiments. Since the graphical model is generated from the simulation code, and the process combines views, the analyst also has a better framework for verifying the coded simulation model. Also, the reverse engineering step provides a structural model useful in converting between different simulation languages or systems. Improvements to the techniques for conversion between languages will facilitate reuse of existing programmed models.     

Bounded model checking of C++ programs based on the Qt cross‐platform framework

The software development process for embedded systems is getting faster and faster, which generally incurs an increase in the associated complexity. As a consequence, technology companies tend to invest in fast and automatic verification mechanisms, to create robust systems and reduce product recall rates. In addition, further development‐time reduction and system robustness can be achieved through cross‐platform frameworks, such as Qt, which favor the reliable port of software stacks to different devices. Based on that, the present paper proposes a simplified version of the Qt framework, which is integrated into a checker based on satisfiability modulo theories (SMT), known as the Efficient SMT‐based Context‐Bounded Model Checker, for verifying actual Qt‐based applications, with a success rate of 89%, for the developed benchmark suite. Furthermore, the simplified version of the Qt framework, named as Qt Operational Model, was also evaluated using other state‐of‐the‐art verifiers for C++ programs. In fact, Qt Operational Model was combined with 2 different verification approaches: explicit‐state model checking and also symbolic (bounded) model checking, during the experimental evaluation, which highlights its flexibility. The proposed methodology is the first one to formally verify Qt‐based applications, which has the potential to devise new directions for software verification of portable code.     

Supporting Software Development With Roles

Software development tools are very important in software engineering. Although roles have been acknowledged and applied for many years in several areas related to software engineering, there is a lack of research on software development tools based on roles. Most significantly, there is no complete and consistent consideration of roles in all the phases of software development. Considering the increasing importance and applications of roles in software development, this paper intends to discuss the importance of roles in software engineering and that of role-based software development; review the literature relevant to role mechanisms in software engineering; propose and describe a role-based software process; and implement a prototype tool for developing complex software systems with the help of role mechanisms     

Component Verification with Automatically Generated Assumptions

Model checking is an automated technique that can be used to determine whether a system satisfies certain required properties. The typical approach to verifying properties of software components is to check them for all possible environments. In reality, however, a component is only required to satisfy properties in specific environments. Unless these environments are formally characterized and used during verification (assume-guarantee paradigm), the results returned by verification can be overly pessimistic. This work introduces an approach that brings a new dimension to model checking of software components. When checking a component against a property, our modified model checking algorithms return one of the following three results: the component satisfies a property for any environment; the component violates the property for any environment; or finally, our algorithms generate an assumption that characterizes exactly those environments in which the component satisfies its required property. Our approach has been implemented in the LTSA tool and has been applied to the analysis of two NASA applications.This paper is an expanded version of Giannakopoulou et al. (2002).     

航天嵌入式软件整数溢出的形式化验证方法

整数溢出引起的软件系统安全性问题屡见不鲜,已有的模型检测技术由于存在状态空间爆炸、不能有效支持中断驱动型程序检测等缺点而少有工程应用.结合真实案例,对航天嵌入式软件整数溢出问题的分布和特征进行了系统性的分析.在有界模型检测技术的基础上,结合整数溢出特征,提出了基于整数溢出变量依赖的程序模型约简技术;同时,针对中断驱动型程序,结合中断函数特征抽象,提出了基于干扰变量的中断驱动程序顺序化方法.经过基准测试程序和真实航天嵌入式软件实验,结果表明：该方法在保证整数溢出问题检出率的前提下,不仅能够提高分析效率,还使得已有的模型检测技术能够适用于中断驱动型程序整数溢出检测.     

广义可能性决策过程的计算树逻辑模型检测

模型检测作为一种形式化验证技术,已被广泛应用于各种并发系统的正确性验证。针对具有非确定性选择和广义可能性分布的并发系统,引入广义可能性决策过程作为此类系统的模型;给出描述其性质的规范语言广义可能性计算树逻辑的概念;研究此类系统的广义可能性计算树逻辑模型检测问题。结论表明,其模型检测算法的时间复杂度也为多项式时间。所获得的结果扩大了广义可能性测度在模型检测中的应用范围。     

Model checking probabilistic social commitments for intelligent agent communication

Interaction among autonomous agents in Multi-Agent Systems (MASs) is a key aspect for agents to coordinate with one another. Social approaches, as opposed to the mental approaches, have recently received a considerable attention in the area of agent communication. They exploit observable social commitments to develop a verifiable formal semantics through which communication protocols can be specified. Developing and implementing algorithmic model checking for social commitments have been recently addressed. However, model checking social commitments in the presence of uncertainty is yet to be investigated.In this paper, we propose a model checking technique for verifying social commitments in uncertain settings. Social commitments are specified in a modal logical language called Probabilistic Computation Tree Logic of Commitments (PCTLC). The modal logic PCTLC extends PCTL, the probabilistic extension of CTL, with modalities for commitments and their fulfillments. The proposed verification method is a reduction-based model checking technique to the model checking of PCTL. The technique is based upon a set of reduction rules that translate PCTLC formulae to PCTL formulae to take benefit of existing model checkers such as PRISM. Proofs that confirm the soundness of the reduction technique are presented. We also present rules that transform our new version of interpreted systems into models of Markov Decision Processes (MDPs) to be suitable for the PRISM tool. We implemented our approach on top of the PRISM model checker and verified some given properties for the Oblivious Transfer Protocol from the cryptography domain. Our simulation demonstrates the effectiveness of our approach in verifying and model checking social commitments in the presence of uncertainty. We believe that the proposed formal verification technique will advance the literature of social commitments in such a way that not only representing social commitments in uncertain settings is doable, but also verifying them in such settings becomes achievable.     

Optimizing symbolic model checking for statecharts

Symbolic model checking based on binary decision diagrams is a powerful formal verification technique for reactive systems. In this paper, we present various optimizations for improving the time and space efficiency of symbolic modal checking for systems specified as statecharts. We used these techniques in our analyses of the models of a collision avoidance system and a fault-tolerant electrical power distribution (EPD) system, both used on commercial aircraft. The techniques together reduce the time and space requirements by orders of magnitude, making feasible some analysis that was previously intractable. We also elaborate on the results of verifying the EPD model. The analysis disclosed subtle modeling and logical flaws not found by simulation     

An overview of model checking practices on verification of PLC software

Programmable logic controllers (PLCs) are heavily used in industrial control systems, because of their high capacity of simultaneous input/output processing capabilities. Characteristically, PLC systems are used in mission critical systems, and PLC software needs to conform real-time constraints in order to work properly. Since PLC programming requires mastering low-level instructions or assembly like languages, an important step in PLC software production is modelling using a formal approach like Petri nets or automata. Afterward, PLC software is produced semiautomatically from the model and refined iteratively. Model checking, on the other hand, is a well-known software verification approach, where typically a set of timed properties are verified by exploring the transition system produced from the software model at hand. Naturally, model checking is applied in a variety of ways to verify the correctness of PLC-based software. In this paper, we provide a broad view about the difficulties that are encountered during the model checking process applied at the verification phase of PLC software production. We classify the approaches from two different perspectives: first, the model checking approach/tool used in the verification process, and second, the software model/source code and its transformation to model checker’s specification language. In a nutshell, we have mainly examined SPIN, SMV, and UPPAAL-based model checking activities and model construction using Instruction Lists (and alike), Function Block Diagrams, and Petri nets/automata-based model construction activities. As a result of our studies, we provide a comparison among the studies in the literature regarding various aspects like their application areas, performance considerations, and model checking processes. Our survey can be used to provide guidance for the scholars and practitioners planning to integrate model checking to PLC-based software verification activities.