共查询到20条相似文献,搜索用时 843 毫秒
1.
异步通讯程序是进程间通过异步消息通讯实现非阻塞并发的程序. 当前异步通讯程序的程序验证问题通常将其归约至向量加法系统及其扩展模型,因而复杂度很高,并缺乏高效工具. 基本并行进程作为向量加法系统的一个子类,其可达性的验证问题为NP完备.首先,本文改进了Osualdo等提出的为异步通讯程序建模的Actor通讯系统, 将其归约至基本并行进程. 然后,实现了基本并行进程的模型检测工具RABLE,实验结果表明,验证方法在异步通讯程序的一系列程序验证问题上具有比已有工具更高效的结果. 相似文献
2.
In this paper, we focus on the verification approach of Metropolis, an integrated design framework for heterogeneous embedded
systems. The verification approach is based on the formal properties specified in Linear Temporal Logic (LTL) or Logic of
Constraints (LOC). Designs may be refined due to synthesis or be abstracted for verification. An automatic abstraction propagation
algorithm is used to simplify the design for specific properties. A user-defined starting point may also be used with automatic
propagation. Two main verification techniques are implemented in Metropolis the formal verification utilizing the model checker
Spin and the simulation trace checking with automatic generated checkers. Translation algorithms from specification models
to verification models, as well as algorithms of generated checkers are discussed. We use several case studies to demonstrate
our approach for verification of system level designs at multiple levels of abstraction. 相似文献
3.
Francesco Maria Donini Marina Mongiello Michele Ruta Rodolfo Totaro 《Electronic Notes in Theoretical Computer Science》2006,151(2):19
Development of Web Applications (WA) needs new methods, techniques and tools to support an engineered project during all the phases of its life cycle. To ensure the reliability of WA it is important they be validated and verified at early design phase. We use Model Checking techniques to perform automated verification of the UML design of a WA.We propose a mathematical model of a WA partitioning the usual Kripke structure into windows, links, pages and actions. Then we specify properties to be checked in a temporal logic, Computation Tree Logic (CTL). Verification is performed adapting the SMV model checker to our formalism. An implemented system that embeds the SMV verifier automatically parses the XMI output of UML tool and builds the SMV model to be verified with respect to specifications. Results of verification proved the benefits of the method. 相似文献
4.
Conrado Daws Marta Kwiatkowska Gethin Norman 《International Journal on Software Tools for Technology Transfer (STTT)》2004,5(2-3):221-236
We report on the automatic verification of timed probabilistic properties of the IEEE 1394 root contention protocol combining two existing tools: the real-time model checker Kronos and the probabilistic model checker Prism. The system is modelled as a probabilistic timed automaton. We first use Kronos to perform a symbolic forwards reachability analysis to generate the set of states that are reachable with non-zero probability from the initial state and before the deadline expires. We then encode this information as a Markov decision process to be analyzed with Prism. We apply this technique to compute the minimal probability of a leader being elected before a deadline, for different deadlines, and study how this minimal probability is influenced by using a biased coin and considering different wire lengths. 相似文献
5.
Graph transformation has recently become more and more popular as a general, rule-based visual specification paradigm to formally capture (a) requirements or behavior of user models (on the model-level), and (b) the operational semantics of modeling languages (on the meta-level) as demonstrated by benchmark applications around the Unified Modeling Language (UML). The current paper focuses on the model checking-based automated formal verification of graph transformation systems used either on the model-level or meta-level. We present a general translation that inputs (i) a metamodel of an arbitrary visual modeling language, (ii) a set of graph transformation rules that defines a formal operational semantics for the language, and (iii) an arbitrary well-formed model instance of the language and generates a transitions system (TS) that serve as the underlying mathematical specification formalism of various model checker tools. The main theoretical benefit of our approach is an optimization technique that projects only the dynamic parts of the graph transformation system into the target transition system, which results in a drastical reduction in the state space. The main practical benefit is the use of existing back-end model checker tools, which directly provides formal verification facilities (without additional efforts required to implement an analysis tool) for many practical applications captured in a very high-level visual notation. The practical feasibility of the approach is demonstrated by modeling and analyzing the well-known verification benchmark of dining philosophers both on the model and meta-level. 相似文献
6.
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. 相似文献
7.
8.
9.
Action Language is a specification language for reactive software systems. In this paper, we present the syntax and the semantics
of the Action Language and we also present an infinite-state symbolic model checker called Action Language Verifier (ALV)
that verifies (or falsifies) CTL properties of Action Language specifications. ALV is built on top of the Composite Symbolic
Library, which is a symbolic manipulator that combines multiple symbolic representations. ALV is a polymorphic model checker
that can use different combinations of the symbolic representations implemented in the Composite Symbolic Library. We describe
the heuristics implemented in ALV for computing fixpoints using the composite symbolic representation. Since Action Language
specifications allow declaration of unbounded integer variables and parameterized integer constants, verification of Action
Language specifications is undecidable. ALV uses several heuristics to conservatively approximate the fixpoint computations.
ALV also implements an automated abstraction technique that enables parameterized verification of a concurrent system with
an arbitrary number of identical processes. 相似文献
10.
Eshuis R. Wieringa R. 《IEEE transactions on pattern analysis and machine intelligence》2004,30(7):437-447
We describe a tool that supports verification of workflow models specified in UML activity diagrams. The tool translates an activity diagram into an input format for a model checker according to a mathematical semantics. With the model checker, arbitrary propositional requirements can be checked against the input model. If a requirement fails to hold, an error trace is returned by the model checker, which our tool presents by highlighting a corresponding path in the activity diagram. We summarize our formal semantics, discuss the techniques used to reduce an infinite state space to a finite one, and motivate the need for strong fairness constraints to obtain realistic results. We define requirement-preserving rules for state space reduction. Finally, we illustrate the whole approach with a few example verifications. 相似文献
11.
Tsuchiya T. Nagano S. Paidi R.B. Kikuno T. 《Parallel and Distributed Systems, IEEE Transactions on》2001,12(1):81-95
A distributed system is said to be self-stabilizing if it converges to safe states regardless of its initial state. In this paper we present our results of using symbolic model checking to verify distributed algorithms against the self-stabilizing property. In general, the most difficult problem with model checking is state explosion; it is especially serious in verifying the self-stabilizing property, since it requires the examination of all possible initial states. So far applying model checking to self-stabilizing algorithms has not been successful due to the problem of state explosion. In order to overcome this difficulty, we propose to use symbolic model checking for this purpose. Symbolic model checking is a verification method which uses Ordered Binary Decision Diagrams (OBDDs) to compactly represent state spaces. Unlike other model checking techniques, this method has the advantage that most of its computations do not depend on the initial states. We show how to verify the correctness of algorithms by means of SMV, a well-known symbolic model checker. By applying the proposed approach to several algorithms in the literature, we demonstrate empirically that the state spaces of self-stabilizing algorithms can be represented by OBDDs very efficiently. Through these case studies, we also demonstrate the usefulness of the proposed approach in detecting errors 相似文献
12.
Felice Balarin 《Electronic Notes in Theoretical Computer Science》2001,23(2):1-10
Interleaved models of computations limit the number of system components that can change states simultaneously. This interleaving constraint often decreases efficiency of symbolic verification methods. It was shown previously that the constraint can be (possibly partially) removed while still preserving safety properties of systems. We propose two extensions of this approach to liveness properties. The first one does not require changes to existing verification algorithms, while the second (which is usually more efficient) does. Our experiments indicate that both approaches can drastically reduce verification time. 相似文献
13.
Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checker 总被引:8,自引:0,他引:8
Statechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modelling
Language (UML). In this paper we present a translation from a subset of UML Statechart Diagrams - covering essential aspects
of both concurrent behaviour, like sequentialisation, parallelism, non-determinism and priority, and state refinement - into
PROMELA, the specification language of the SPIN model checker. SPIN is one of the most advanced analysis and verification
tools available nowadays. Our translation allows for the automatic verification of UML Statechart Diagrams. The translation
is simple, proven correct, and promising in terms of state space representation efficiency.
Received September 1999 / Accepted in revised form February 2000 相似文献
14.
Andreas Griesmayer Stefan Staber Roderick Bloem 《Electronic Notes in Theoretical Computer Science》2007,174(4):95
If a program does not fulfill a given specification, a model checker delivers a counterexample, a run which demonstrates the wrong behavior. Even with a counterexample, locating the actual fault in the source code is often a difficult task for the verification engineer.We present an automatic approach for fault localization in C programs. The method is based on model checking and reports only components that can be changed such that the difference between actual and intended behavior of the example is removed. To identify these components, we use the bounded model checker CBMC on an instrumented version of the program. We present experimental data that supports the applicability of our approach. 相似文献
15.
Binary synchronization has been used extensively in the construction of mathematical models for the verification of embedded
systems. Although it allows for the modeling of complex cooperation among many processes in a natural environment, not many
tools have been developed to support the modeling capability in this regard. In this article, we first give examples to argue
that special algorithms are needed for the efficient verification of systems with complex synchronizations. We then define
our models of distributed real-time systems with synchronized cooperation among many processes. We present algorithms for
the construction of BDD-like diagrams for the characterization of complex synchronizations among many processes. We present
weakest precondition algorithms that take advantage of the just-mentioned BDD-like diagrams for the efficient verification
of complex real-time systems. Finally, we report experiments and argue that the techniques could be useful in practice. 相似文献
16.
17.
Jiří BarnatAuthor Vitae Petr BauchAuthor VitaeLuboš BrimAuthor Vitae Milan Češka 《Journal of Parallel and Distributed Computing》2012
Recent technological developments made various many-core hardware platforms widely accessible. These massively parallel architectures have been used to significantly accelerate many computation demanding tasks. In this paper, we show how the algorithms for LTL model checking can be redesigned in order to accelerate LTL model checking on many-core GPU platforms. Our detailed experimental evaluation demonstrates that using the NVIDIA CUDA technology results in a significant speedup of the verification process. Together with state space generation based on shared hash-table and DFS exploration, our CUDA accelerated model checker is the fastest among state-of-the-art shared memory model checking tools. 相似文献
18.
Aaron Stump Clark W. Barrett David L. Dill 《Electronic Notes in Theoretical Computer Science》2002,70(2)
Software that can produce independently checkable evidence for the correctness of its output has received recent attention for use in certifying compilers and proof-carrying code. CVC (Cooperating Validity Checker) is a proof-producing validity checker for a decidable fragment of first-order logic enriched with background theories. This paper describes how proofs of valid formulas are produced from the decision procedure for linear real arithmetic implemented in CVC. It is shown how extensions to LF which support proof rules schematic in an arity (“elliptical” rules) are very convenient for this purpose. 相似文献
19.
20.
Holzmann G.J. Bosnacki D. 《IEEE transactions on pattern analysis and machine intelligence》2007,33(10):659-674
We describe an extension of the SPIN model checker for use on multicore shared-memory systems and report on its performance. We show how, with proper load balancing, the time requirements of a verification run can, in some cases, be reduced close to N-fold when N processing cores are used. We also analyze the types of verification problems for which multicore algorithms cannot provide relief. The extensions discussed here require only relatively small changes in the SPIN source code and are compatible with most existing verification modes such as partial order reduction, the verification of temporal logic formulas, bitstate hashing, and hash-compact compression. 相似文献