The software model checker Blast

Blast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, Blast either statically proves that the program satisfies the safety property, or provides an execution path that exhibits a violation of the property (or, since the problem is undecidable, does not terminate). Blast constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. This paper gives an introduction to Blast and demonstrates, through two case studies, how it can be applied to program verification and test-case generation. In the first case study, we use Blast to statically prove memory safety for C programs. We use CCured, a type-based memory-safety analyzer, to annotate a program with run-time assertions that check for safe memory operations. Then, we use Blast to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate execution scenarios that violate the assertions for the remaining run-time checks. In our second case study, we use Blast to automatically generate test suites that guarantee full coverage with respect to a given predicate. Given a C program and a target predicate p, Blast determines the program locations q for which there exists a program execution that reaches q with p true, and automatically generates a set of test vectors that cause such executions. Our experiments show that Blast can provide automated, precise, and scalable analysis for C programs.     

A logic-based agent that plans for extended reachability goals

Planning to reach a goal is an essential capability for rational agents. In general, a goal specifies a condition to be achieved at the end of the plan execution. In this article, we introduce nondeterministic planning for extended reachability goals (i.e., goals that also specify a condition to be preserved during the plan execution). We show that, when this kind of goal is considered, the temporal logic ctl turns out to be inadequate to formalize plan synthesis and plan validation algorithms. This is mainly due to the fact that the ctl’s semantics cannot discern among the various actions that produce state transitions. To overcome this limitation, we propose a new temporal logic called α-ctl. Then, based on this new logic, we implement a planner capable of synthesizing reliable plans for extended reachability goals, as a side effect of model checking.     

基于总线技术的实时通信方法研究与应用

针对武器装备ARINC429总线实时性要求高的问题,本文提出一种基于RTX实时操作系统的ARINC429总线实时通信方法并进行了应用。本文方法在PXI总线AMC5206B的基础上,搭建了软硬件环境,设计了Windows应用程序和RTX应用程序,通过共享内存进行数据传递,实现了RTSS进程在测试主流程的嵌入。设计了板卡在RTX系统下的驱动程序,实现了中断触发数据读取,提高了程序效率。最后,通过Windows应用程序实验验证了本文方法的功能,并具有实时性强,通用性好等优点。     

RTX 平台下实时全软件数控雕刻系统

计算机仿真设计与制造需要极高的实时性和可控性,由于Windows操作系统本身实时性的缺陷,给计算机仿真应用带来了一些不确定因素.经过充分论证,引入了IntervalZero公司的基于Windows的实时仿真解决方案RTX,并结合某型号数控雕刻机的设计要求,总结出了Windows环境下RTX实时仿真应用系统的设计方法及RTX环境下全软件数控雕刻系统主要功能模块程序编写,并将这种设计方法成功应用于某数控雕刻系统中.实际雕刻实例表明RTX平台下全软件程序能够满足数控雕刻系统对实时性要求.     

A Top-Down Approach to Search-Trees: Improved Algorithmics for 3-Hitting Set

In this paper, we show how to systematically improve on parameterized algorithms and their analysis, focusing on search-tree based algorithms for 3-Hitting Set. We concentrate on algorithms which are easy to implement, in contrast with the highly sophisticated algorithms which have been designed previously to improve on the exponential base in the algorithms. However, this necessitates a more complex algorithm analysis based on a so-called auxiliary parameter, a technique which we believe can be used in other circumstances, as well.     

Automatically configuring constraint satisfaction programs: A case study

Multi-tac is a learning system that synthesizes heuristic constraint satisfaction programs. The system takes a library of generic algorithms and heuristics and specializes them for a particular application. We present a detailed case study with three different distributions of a single combinatorial problem, Minimum Maximal Matching, and show that Muti-tac can synthesize programs for these different distributions that perform on par with hand-coded programs and that exceed the performance of some well-known satisfiability algorithms. In synthesizing a program, Multi-tac bases its choice of heuristics on an instance distribution, and we demonstrate that this capability has a significant impact on the results.     

基于RTX的工程飞行模拟器数据采集与存储系统设计

在一些仿真应用中,由于Windows操作系统较差的实时性,从而给许多半物理仿真试验带来了一些不确定的因素.在充分论证的基础上,引入了Ardence公司的基于Windows的硬实时解决方案RTX（Real-Time eXtension）,并结合某型号飞行器仿真课题总结出了Windows环境下RTX实时应用系统的设计方法与开发流程以及RTX下硬件板卡驱动程序的编写,最后将这种设计方法成功应用在某型号飞行器飞行仿真系统中.实验证明该仿真系统是可靠的、稳定的,整个实验过程中飞行器的飞行数据没有丢失,仿真周期确定,结果正确,RTX仿真程序能够满足系统对实时性和确定性的要求.     

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.     

Reflection and time-dependent computing: Experiences with the R2 architecture

In this paper we present an application of computational reflection in the programming oftime-dependent systems. A time-dependent system performs its tasks according to timing specifications specified within the system or imposed from outside the system. Reflective techniques can be applied to programming time-dependent systems because (1) some application programs require the introduction of a new language construct for specifying timing requirements and (2) different applications may require domain-specific scheduling algorithms. To allow a programmer to add or modify language constructs or scheduling algorithms, however, a clear reflective architecture and program interfaces must be provided. This paper proposes a concurrent object-based reflective architecture (R ² architecture) for time-dependent computing. This architecture is based on anindividual reflection scheme and introduces new meta-level objects (real-time meta objects) that are responsible for time-dependent capabilities. An alarm-clock object and a scheduler object are introduced, and message protocols between them and real-time meta objects are defined. We implemented this architecture on ABCL/R2 and created the Sampled Sound Player program as an application. With this application we provided three different scheduler objects and measured the impact of different scheduling algorithms on sound playback. The measured results show that a scheduler with more complex computations at the meta level exhibited less scheduling overhead, thus was capable of better sound playback. The other example, Time-dependent Graceful Degradation Scheme, demonstrates the programming of functionality degradation triggered by failure to satisfy timing specifications.     

Verification of clocked and hybrid systems

This paper presents a new computational model for real-time systems, called the clocked transition system (CTS) model. The CTS model is a development of our previous timed transition model, where some of the changes are inspired by the model of timed automata. The new model leads to a simpler style of temporal specification and verification, requiring no extension of the temporal language. We present verification rules for proving safety a nd liveness properties of clocked transition systems. All rules are associated with verification diagrams. The verification of response properties requires adjustments of the proof rules developed for untimed systems, reflecting the fact that progress in the real time systems is ensured by the progress of time and not by fairness. The style of the verification rules is very close to the verification style of untimed systems which allows the (re)use of verification methods and tools, developed for u ntimed reactive systems, for proving all interesting properties of real-time systems. We conclude with the presentation of a branching-time based approach for verifying that an arbitrary given CTS isnon-zeno. Finally, we present an extension of the model and the invariance proof rule for hybrid systems. Received: 23 September 1998 / 7 June 1999     

CAESAR_SOLVE: A generic library for on-the-fly resolution of alternation-free Boolean equation systems

Boolean equation systems (Bess) provide a useful framework for modeling various verification problems on finite-state concurrent systems, such as equivalence checking and model checking. These problems can be solved on the fly (i.e., without constructing explicitly the state space of the system under analysis) by using a demand-driven construction and resolution of the corresponding Bes. In this article, we present a generic software library dedicated to on-the-fly resolution of alternation-free Bess. Four resolution algorithms are currently provided by the library: algorithms A1 and A2 are general, the latter being optimized to produce small-depth diagnostics, whereas algorithms A3 and A4 are specialized for handling acyclic and disjunctive/conjunctive Bess in a memory-efficient way. The library has been developed within the Cadp verification toolbox using the generic Open/Caesar environment and is currently used for three purposes: on-the-fly equivalence checking modulo five widely used equivalence relations, on-the-fly model checking of regular alternation-free modal μ-calculus, and on-the-fly reduction of state spaces based on τ-confluence .     

Slicing communicating automata specifications: polynomial algorithms for model reduction

In the industry, communicating automata specifications are mainly used in fields where the reliability requirements are high, as this formalism allow the use of powerful validation tools. Still, on large scale industrial specifications, formal methods suffer from the combinatorial explosion phenomenon. In our contribution, we suggest to try to bypass this phenomenon, in applying slicing techniques preliminarily to the targeted complex analysis. This analysis can thus be performed a posteriori on a reduced (or sliced) specification, which is potentially less exposed to combinatorial explosion. The slicing method is based on dependence relations, defined on the specification under analysis, and is mainly founded on the literature on compiler construction and program slicing. A theoretical framework is described, for static analyses of communicating automata specifications. This includes formal definitions for the aforementioned dependence relations, and for a slice of a specification with respect to a slicing criterion. Efficient algorithms are also described in detail, for calculating dependence relations and specification slices. Each of these algorithms has been shown to be polynomial, and sound and complete with respect to its respective definition. These algorithms have also been implemented in a slicing tool, named Carver, that has shown to be operational in specification debugging and understanding. The experimental results obtained in model reduction with this tool are promising, notably in the area of formal validation and verification methods, e.g.model checking, test case generation.     

Algorithm portfolio selection as a bandit problem with unbounded losses

We propose a method that learns to allocate computation time to a given set of algorithms, of unknown performance, with the aim of solving a given sequence of problem instances in a minimum time. Analogous meta-learning techniques are typically based on models of algorithm performance, learned during a separate offline training sequence, which can be prohibitively expensive. We adopt instead an online approach, named GAMBLETA, in which algorithm performance models are iteratively updated, and used to guide allocation on a sequence of problem instances. GAMBLETA is a general method for selecting among two or more alternative algorithm portfolios. Each portfolio has its own way of allocating computation time to the available algorithms, possibly based on performance models, in which case its performance is expected to improve over time, as more runtime data becomes available. The resulting exploration-exploitation trade-off is represented as a bandit problem. In our previous work, the algorithms corresponded to the arms of the bandit, and allocations evaluated by the different portfolios were mixed, using a solver for the bandit problem with expert advice, but this required the setting of an arbitrary bound on algorithm runtimes, invalidating the optimal regret of the solver. In this paper, we propose a simpler version of GAMBLETA, in which the allocators correspond to the arms, such that a single portfolio is selected for each instance. The selection is represented as a bandit problem with partial information, and an unknown bound on losses. We devise a solver for this game, proving a bound on its expected regret. We present experiments based on results from several solver competitions, in various domains, comparing GAMBLETA with another online method.     

Rigorous automated network security management

Achieving a security goal in a networked system requires the cooperation of a variety of devices, each device potentially requiring a different configuration. Many information security problems may be solved with appropriate models of these devices and their interactions, giving a systematic way to handle the complexity of real situations.We present an approach, rigorous automated network security management, that front-loads formal modeling and analysis before problem solving, thereby providing easy-to-run tools with rigorously justified results. With this approach, we model the network and a class of practically important security goals. The models derived suggest algorithms that, given system configuration information, determine the security goals satisfied by the system. The modeling provides rigorous justification for the algorithms, which may then be implemented as ordinary computer programs requiring no formal methods training to operate.We have applied this approach to several problems. In this paper we describe two: distributed packet filtering and the use of IP security (IPsec) gateways. We also describe how to piece together the two separate solutions to these problems, jointly enforcing packet filtering as well as IPsec authentication and confidentiality on a single network.     

Algorithms for finding directed graph isomorphisms by finite automata

The determination of the isomorphisms between two directed graphs based on those between the corresponding one-input Moore machines plus an additional condition to be checked is developed. Without this condition, the Moore machine isomorphism problem is not equivalent to the graph isomorphism problem. Two algorithms are devised for solving the graph isomorphism problem based on the above method. These algorithms are implemented aspl/1 programs, executed on an IBM System 370/158, experimentally analyzed by a random graph generating program and abal assembly language time routine, and illustrated by examples. The experimental data for the class of isomorphicn/2 regular graphs are fitted by quadratic equations of the input size. In addition the worst-case complexities of both algorithms are found.     

Some Computational Aspects of distance-sat

In many AI fields, one must face the problem of finding a solution that is as close as possible to a given configuration. This paper addresses this problem in a propositional framework. We introduce the decision problem distance-sat, which consists in determining whether a propositional formula admits a model that disagrees with a given partial interpretation on at most d variables. The complexity of distance-sat and of several restrictions of it are identified. Two algorithms based on the well-known Davis/Logemann/Loveland search procedure for the satisfiability problem sat are presented so as to solve distance-sat for CNF formulas. Their computational behaviors are compared with the ones offered by sat solvers on sat encodings of distance-sat instances. The empirical evaluation allows us to draw firm conclusions about the respective performances of the algorithms and to relate the difficulty of distance-sat with the difficulty of sat from the practical side. A preliminary version of this paper appeared with the title “distance-sat: Complexity and Algorithms” in the proceedings of the 16 ^th National Conference on Artificial Intelligence (AAAI’99), pages 642–647, 1999.     

Approximation algorithms for scheduling real-time jobs with multiple feasible intervals

Time-critical jobs in many real-time applications have multiple feasible intervals. Such a job is constrained to execute from start to completion in one of its feasible intervals. A job fails if the job remains incomplete at the end of the last feasible interval. Earlier works developed an optimal off-line algorithm to schedule all the jobs in a given job set and on-line heuristics to schedule the jobs in a best effort manner. This paper is concerned with how to find a schedule in which the number of jobs completed in one of their feasible intervals is maximized. We show that the maximization problem is -hard for both non-preemptible and preemptible jobs. This paper develops two approximation algorithms for non-preemptible and preemptible jobs. When jobs are non-preemptible, Algorithm Least Earliest Completion Time First (LECF) is shown to have a 2-approximation factor; when jobs are preemptible, Algorithm Least Execution Time First (LEF) is proved being a 3-approximation algorithm. We show that our analysis for the two algorithms are tight. We also evaluate our algorithms by extensive simulations. Simulation results show that Algorithms LECF and LEF not only guarantee the approximation factors but also outperform other multiple feasible interval scheduling algorithms in average.     

On Two Techniques of Combining Branching and Treewidth

Branch & Reduce and dynamic programming on graphs of bounded treewidth are among the most common and powerful techniques used in the design of moderately exponential time exact algorithms for NP hard problems. In this paper we discuss the efficiency of simple algorithms based on combinations of these techniques. The idea behind these algorithms is very natural: If a parameter like the treewidth of a graph is small, algorithms based on dynamic programming perform well. On the other side, if the treewidth is large, then there must be vertices of high degree in the graph, which is good for branching algorithms. We give several examples of possible combinations of branching and programming which provide the fastest known algorithms for a number of NP hard problems. All our algorithms require non-trivial balancing of these two techniques. In the first approach the algorithm either performs fast branching, or if there is an obstacle for fast branching, this obstacle is used for the construction of a path decomposition of small width for the original graph. Using this approach we give the fastest known algorithms for Minimum Maximal Matching and for counting all 3-colorings of a graph. In the second approach the branching occurs until the algorithm reaches a subproblem with a small number of edges (and here the right choice of the size of subproblems is crucial) and then dynamic programming is applied on these subproblems of small width. We exemplify this approach by giving the fastest known algorithm to count all minimum weighted dominating sets of a graph. We also discuss how similar techniques can be used to design faster parameterized algorithms. A preliminary version of this paper appeared as Branching and Treewidth Based Exact Algorithms in the Proceedings of the 17th International Symposium on Algorithms and Computation (ISAAC 2006) [15]. Additional support by the Research Council of Norway.     

Bounded model checking of software using SMT solvers instead of SAT solvers

C bounded model checking (cbmc) has proved to be a successful approach to automatic software analysis. The key idea is to (i) build a propositional formula whose models correspond to program traces (of bounded length) that violate some given property and (ii) use state-of-the-art SAT solvers to check the resulting formulae for satisfiability. In this paper, we propose a generalisation of the cbmc approach on the basis of an encoding into richer (but still decidable) theories than propositional logic. We show that our approach may lead to considerably more compact formulae than those obtained with cbmc. We have built a prototype implementation of our technique that uses a satisfiability modulo theories (SMT) solver to solve the resulting formulae. Computer experiments indicate that our approach compares favourably with—and on some significant problems outperforms—cbmc.     

Making Use of the Most Expressive Jumping Emerging Patterns for Classification

Classification aims to discover a model from training data that can be used to predict the class of test instances. In this paper, we propose the use of jumping emerging patterns (JEPs) as the basis for a new classifier called the JEP-Classifier. Each JEP can capture some crucial difference between a pair of datasets. Then, aggregating all JEPs of large supports can produce a more potent classification power. Procedurally, the JEP-Classifier learns the pair-wise features (sets of JEPs) contained in the training data, and uses the collective impacts contributed by the most expressive pair-wise features to determine the class labels of the test data. Using only the most expressive JEPs in the JEP-Classifier strengthens its resistance to noise in the training data, and reduces its complexity (as there are usually a very large number of JEPs). We use two algorithms for constructing the JEP-Classifier which are both scalable and efficient. These algorithms make use of the border representation to efficiently store and manipulate JEPs. We also present experimental results which show that the JEP-Classifier achieves much higher testing accuracies than the association-based classifier of (Liu et al, 1998), which was reported to outperform C4.5 in general. Received 31 May 2000 / Revised 7 August 2000 / Accepted in revised form 28 August 2000