Model checking C source code for embedded systems

In this paper, the applicability of model checking to C code for embedded systems is studied. The paper is divided into two parts. In the first part, 13 existing model checkers for C code are detailed and evaluated for their applicability in the verification of C code for embedded systems. A case study is presented that applied CBMC as one representative C code model checker to an exemplary microcontroller program. As a consequence of this case study, we decided to develop a new model checker for source code for microcontrollers, called [mc]square. It is described in the second part of this paper. We present the architecture and the peculiarities of [mc]square, and we successfully applied [mc]square to the same microcontroller program used in the case study.     

Model driven code checking

Model checkers were originally developed to support the formal verification of high-level design models of distributed system designs. Over the years, they have become unmatched in precision and performance in this domain. Research in model checking has meanwhile moved towards methods that allow us to reason also about implementation level artifacts (e.g., software code) directly, instead of hand-crafted representations of those artifacts. This does not mean that there is no longer a place for the use of high-level models, but it does mean that such models are used in a different way today. In the approach that we describe here, high-level models are used to represent the environment for which the code is to be verified, but not the application itself. The code of the application is now executed as is by the model checker, while using powerful forms of abstraction on-the-fly to build the abstract state space that guides the verification process. This model-driven code checking method allows us to verify implementation level code efficiently for high-level safety and liveness properties. In this paper, we give an overview of the methodology that supports this new paradigm of code verification.     

Boolean and Cartesian abstraction for model checking C programs

We show how to attack the problem of model checking a C program with recursive procedures using an abstraction that we formally define as the composition of the Boolean and the Cartesian abstractions. It is implemented through a source-to-source transformation into a Boolean C program; we give an algorithm to compute the transformation with a cost that is exponential in its theoretical worst-case complexity but feasible in practice.     

模型检测迷惑二进制恶意代码

对二进制恶意代码进行形式化建模,开发了一个检查迷惑恶意代码的模型检查器。生成迷惑前的二进制恶意代码的有限状态机模型,再使用模型检查器检测迷惑二进制恶意代码,如果迷惑二进制恶意代码能被有限状态机模型识别,可判定其为恶意代码。实验结果表明模型检查迷惑二进制恶意代码是一种有效的静态分析方法,可以检测出一些常用的迷惑恶意代码。     

Model checking Petri nets with names using data-centric dynamic systems

Petri nets with name creation and management (\({\nu}\)-PNs) have been recently introduced as an expressive model for dynamic (distributed) systems, whose dynamics are determined not only by how tokens flow in the system, but also by the pure names they carry. On the one hand, this extension makes the resulting nets strictly more expressive than P/T nets: they can be exploited to capture a plethora of interesting systems, such as distributed systems enriched with channels and name passing, service interaction with correlation mechanisms, and resource-constrained workflow nets that explicitly account for process instances. On the other hand, fundamental properties like coverability, termination and boundedness are decidable for \({\nu}\)-PNs. In this work, we go one step beyond the verification of such general properties, and provide decidability and undecidability results of model checking \({\nu}\)-PNs against variants of first-order \({\mu}\)-calculus, recently proposed in the area of data-aware process analysis. While this model checking problem is undecidable in the general case, decidability can be obtained by considering different forms of boundedness, which still give raise to an infinite-state transition system. We then ground our framework to tackle the problem of soundness checking over workflow nets enriched with explicit process instances and resources. Notably, our decidability results are obtained via a translation to data-centric dynamic systems, a recently devised framework for the formal specification and verification of data-aware business processes working over full-fledged relational databases with constraints. In this light, our results contribute to the cross-fertilization between the area of formal methods for concurrent systems and that of foundations of data-aware processes, which has not been extensively investigated so far.     

Model checking agent programming languages

In this paper we describe a verification system for multi-agent programs. This is the first comprehensive approach to the verification of programs developed using programming languages based on the BDI (belief-desire-intention) model of agency. In particular, we have developed a specific layer of abstraction, sitting between the underlying verification system and the agent programming language, that maps the semantics of agent programs into the relevant model-checking framework. Crucially, this abstraction layer is both flexible and extensible; not only can a variety of different agent programming languages be implemented and verified, but even heterogeneous multi-agent programs can be captured semantically. In addition to describing this layer, and the semantic mapping inherent within it, we describe how the underlying model-checker is driven and how agent properties are checked. We also present several examples showing how the system can be used. As this is the first system of its kind, it is relatively slow, so we also indicate further work that needs to be tackled to improve performance.     

Type inference and strong static type checking for Promela

The Spin model checker and its specification language Promela have been used extensively in industry and academia to check the logical properties of distributed algorithms and protocols. Model checking with Spin involves reasoning about a system via an abstract Promela specification, thus the technique depends critically on the soundness of this specification. Promela includes a rich set of data types including first-class channels, but the language syntax restricts the declaration of channel types so that it is not generally possible to deduce the complete type of a channel directly from its declaration. We present the design and implementation of Etch, an enhanced type checker for Promela, which uses constraint-based type inference to perform strong type checking of Promela specifications, allowing static detection of errors that Spin would not detect until simulation/verification time, or that Spin may miss completely. We discuss theoretical and practical problems associated with designing a type system and type checker for an existing language, and formalise our approach using a Promela-like calculus. To handle subtyping between base types, we present an extension to a standard unification algorithm to solve a system of equality and subtyping constraints, based on bounded substitutions.     

嵌入式程序设计中C/C++代码的优化

本文介绍了在嵌入式程序设计中几种提高C/C 代码效率的方法，通过对例子的分析，探讨了影响程序效率的原因。     

Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement

The stochastic dynamics of biochemical reaction networks can be modeled using a number of succinct formalisms all of whose semantics are expressed as Continuous Time Markov Chains (CTMC). While some kinetic parameters for such models can be measured experimentally, most are estimated by either fitting to experimental data or by performing ad hoc, and often manual search procedures. We consider an alternative strategy to the problem, and introduce algorithms for automatically synthesizing the set of all kinetic parameters such that the model satisfies a given high-level behavioral specification. Our algorithms, which integrate statistical model checking and abstraction refinement, can also report the infeasibility of the model if no such combination of parameters exists. Behavioral specifications can be given in any finitely monitorable logic for stochastic systems, including the probabilistic and bounded fragments of linear and metric temporal logics. The correctness of our algorithms is established using a novel combination of arguments based on survey sampling and uniform continuity. We prove that the probability of a measurable set of paths is uniformly and jointly continuous with respect to the kinetic parameters. Under a suitable technical condition, we also show that the unbiased statistical estimator for the probability of a measurable set of paths is monotonic in the parameter space. We apply our algorithms to two benchmark models of biochemical signaling, and demonstrate that they can efficiently find parameter regimes satisfying a given high-level behavioral specification. In particular, we show that our algorithms can synthesize up to 6 parameters, simultaneously, which is more than that reported by any other synthesis algorithm for stochastic systems. Moreover, when parameter estimation is desired, as opposed to synthesis, we show that our approach can scale to even higher dimensional spaces, by identifying the single parameter combination that maximizes the probability of the behavior being true in an 11-dimensional system.     

Automatic abstraction controller in reinforcement learning agent via automata

Reinforcement learning (RL) for solving large and complex problems faces the curse of dimensions problem. To overcome this problem, frameworks based on the temporal abstraction have been presented; each having their advantages and disadvantages. This paper proposes a new method like the strategies introduced in the hierarchical abstract machines (HAMs) to create a high-level controller layer of reinforcement learning which uses options. The proposed framework considers a non-deterministic automata as a controller to make a more effective use of temporally extended actions and state space clustering. This method can be viewed as a bridge between option and HAM frameworks, which tries to suggest a new framework to decrease the disadvantage of both by creating connection structures between them and at the same time takes advantages of them. Experimental results on different test environments show significant efficiency of the proposed method.     

Infinite-state invariant checking with IC3 and predicate abstraction

We address the problem of verifying invariant properties on infinite-state systems. We present a novel approach, IC3ia, for generalizing the IC3 invariant checking algorithm from finite-state to infinite-state transition systems, expressed over some background theories. The procedure is based on a tight integration of IC3 with Implicit Abstraction, a form of predicate abstraction that expresses abstract paths without computing explicitly the abstract system. In this scenario, IC3 operates only at the Boolean level of the abstract state space, discovering inductive clauses over the abstraction predicates. Theory reasoning is confined within the underlying SMT solver, and applied transparently when performing satisfiability checks. When the current abstraction allows for a spurious counterexample, it is refined by discovering and adding a sufficient set of new predicates. Importantly, this can be done in a completely incremental manner, without discarding the clauses found in the previous search. The proposed approach has two key advantages. First, unlike previous SMT generalizations of IC3, it allows to handle a wide range of background theories without relying on ad-hoc extensions, such as quantifier elimination or theory-specific clause generalization procedures, which might not always be available and are often highly inefficient. Second, compared to a direct exploration of the concrete transition system, the use of abstraction gives a significant performance improvement, as our experiments demonstrate.     

Model checking temporal knowledge and commitments in multi-agent systems using reduction

Though modeling and verifying Multi-Agent Systems (MASs) have long been under study, there are still challenges when many different aspects need to be considered simultaneously. In fact, various frameworks have been carried out for modeling and verifying MASs with respect to knowledge and social commitments independently. However, considering them under the same framework still needs further investigation, particularly from the verification perspective. In this article, we present a new technique for model checking the logic of knowledge and commitments (CTLKC⁺). The proposed technique is fully-automatic and reduction-based in which we transform the problem of model checking CTLKC⁺ into the problem of model checking an existing logic of action called ARCTL. Concretely, we construct a set of transformation rules to formally reduce the CTLKC⁺ model into an ARCTL model and CTLKC⁺ formulae into ARCTL formulae to get benefit from the extended version of NuSMV symbolic model checker of ARCTL. Compared to a recent approach that reduces the problem of model checking CTLKC⁺ to another logic of action called GCTL¹, our technique has better scalability and efficiency. We also analyze the complexity of the proposed model checking technique. The results of this analysis reveal that the complexity of our reduction-based procedure is PSPACE-complete for local concurrent programs with respect to the size of these programs and the length of the formula being checked. From the time perspective, we prove that the complexity of the proposed approach is P-complete with regard to the size of the model and length of the formula, which makes it efficient. Finally, we implement our model checking approach on top of extended NuSMV and report verification results for the verification of the NetBill protocol, taken from business domain, against some desirable properties. The obtained results show the effectiveness of our model checking approach when the system scales up.     

Model checking fault tolerant systems

This paper proposes a modelling approach suitable for formalizing fault tolerant systems, taking into account different fault scenarios. Verification of the properties of such systems is then performed using model checking. A general framework for the formal specification and verification of fault tolerant systems is defined starting from these principles, and experience with its application to two case studies is then presented. Copyright © 2002 John Wiley & Sons, Ltd.     

Model checking real-time value-passing systems

In this paper, to model check real-time value-passing systems, a formal language Timed Symbolic Transition Graph and a logic system named Timed Predicate p-Calculus are proposed. An algorithm is presented which is local in that it generates and investigates the reachable state space in top-down fashion and maintains the partition for time evaluations as coarse as possible while on-the-fly instantiating data variables. It can deal with not only data variables with finite value domain, but also the so called data independent variables with infinite value domain. To authors knowledge, this is the first algorithm for model checking timed systems containing value-passing features.     

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.     

Model checking with fairness assumptions using PAT

Recent development on distributed systems has shown that a variety of fairness constraints (some of which are only recently defined) play vital roles in designing self-stabilizing population protocols. Existing model checkers are deficient in verifying the systems as only limited kinds of fairness are supported with limited verification efficiency. In this work, we support model checking of distributed systems in the toolkit PAT (process analysis toolkit), with a variety of fairness constraints (e.g., process-level weak/strong fairness, event-level weak/strong fairness, strong global fairness). It performs on-the-fly verification against linear temporal properties. We show through empirical evaluation (on recent population protocols as well as benchmark systems) that PAT has advantage in model checking with fairness. Previously unknown bugs have been revealed against systems which are designed to function only with strong global fairness.     

适用于嵌入式系统的QR码识别算法

针对一般情况下采集到的条码图像,提出了一种适用于嵌入式系统的自动识别算法,并在NIOS嵌入式系统上进行了验证。实验表明,该算法能够快速准确地提取条码符号信息,效果良好。     

嵌入式系统中的代码动态链接模型

飞行器上的计算机系统软件有时需要更新或升级,为了增加软件更新或升级的灵活性,降低其代价,有必要根据功能对飞行器上的软件进行模块划分,以实现单模块可更新升级.为此,提出了一种适用于嵌入式系统的代码动态链接模型,并以具体项目为背景,阐述了其编程实现的关键部分.该模型为嵌入式系统中软件目标代码复用和软件模块升级奠定了基础,在小卫星等空间飞行器上具有一定的应用价值.     

Mobile code daemons for networks of embedded systems

Originally implemented to support wireless sensor networks, the lightweight mobile code daemons works on wired networks as well. The mobile code daemon we present is based on a core network protocol called the remote execution and action protocol (REAP), which is responsible for passing messages between nodes within our network. The authors have implemented them to run on multiple operating systems and architectures. The daemons use a peer-to-peer indexing scheme to find mobile code packages as needed. Calls to the daemons are automatically dereferenced to find the proper package for a node's OS and hardware.