共查询到20条相似文献,搜索用时 15 毫秒
1.
Moataz Kamel Stefan Leue 《International Journal on Software Tools for Technology Transfer (STTT)》2000,2(4):394-409
The General Inter-Orb Protocol (GIOP) is a key component of the Common Object Request Broker Architecture (CORBA) specification.
We present the formal modeling and validation of the GIOP protocol using the Promela language, Linear Time Temporal Logic
(LTL) and the Spin model checker. We validate the Promela model using ten high-level requirements which we elicit from the
informal CORBA specification. These requirements are then formalized in LTL and the Spin model checker is used to determine
their validity. During the validation process we discovered a few problems in GIOP: a potential transport-layer interface
deadlock and problems with the server migration protocol. We also describe how property specification patterns helped us in
formalizing the high-level requirements that we have elicited. 相似文献
2.
On-the-fly conformance testing using SPIN 总被引:3,自引:1,他引:2
René G. de Vries Jan Tretmans 《International Journal on Software Tools for Technology Transfer (STTT)》2000,2(4):382-393
3.
4.
Verification and optimization of a PLC control schedule 总被引:1,自引:0,他引:1
Ed Brinksma Angelika Mader Ansgar Fehnker 《International Journal on Software Tools for Technology Transfer (STTT)》2002,4(1):21-33
We report on the use of model checking techniques for both the verification of a process control program and the derivation
of optimal control schedules. Most of this work has been carried out as part of a case study for the EU VHS project (Verification
of Hybrid Systems), in which the program for a Programmable Logic Controller (PLC) of an experimental chemical plant had to
be designed and verified. The original intention of our approach was to see how much could be achieved here using the standard
model checking environment of SPIN/Promela. As the symbolic calculations of real-time model checkers can be quite expensive
it is interesting to try and exploit the efficiency of established non-real-time model checkers like SPIN in those cases where
promising work-arounds seem to exist. In our case we handled the relevant real-time properties of the PLC controller using
a time-abstraction technique; for the scheduling we implemented in Promela a so-called variable time advance procedure . To
compare and interpret the results we carried out the same case study with the aid of the real-time model checker Uppaal, enhanced
with facilities for cost-guided state space exploration. Both approaches proved sufficiently powerful to verify the design
of the controller and/or derive (time-)optimal schedules within reasonable time and space requirements.
Published online: 2 October 2002
The work reported here was carried out while the second and third authors were employed by the Computer Science Department
of the University of Nijmegen, Netherlands. The second author was supported by an NWO postdoc grant, the third author by an
NWO PhD grant, and both were supported by the EU LTR project VHS (Project No. 26270). 相似文献
5.
Symmetric Spin 总被引:1,自引:0,他引:1
Dragan Bošnački Dennis Dams Leszek Holenderski 《International Journal on Software Tools for Technology Transfer (STTT)》2002,4(1):92-106
6.
James C. Corbett Matthew B. Dwyer John Hatcliff Robby 《International Journal on Software Tools for Technology Transfer (STTT)》2002,4(1):34-56
Research on how to reason about correctness properties of software systems using model checking is advancing rapidly. Work
on extracting finite-state models from program source code and on abstracting those models is focused on enabling the tractable
checking of program properties such as freedom from deadlock and assertion violations. For the most part, the problem of specifying
more general program properties has not been considered. In this paper, we report on the support for specifying properties
of dynamic multi-threaded Java programs that we have built into the Bandera system. Bandera extracts finite-state models,
in the input format of several existing model checkers, from Java code based on the property to be checked. The Bandera Specification
Language (BSL) provides a language for defining general assertions and pre/post conditions on methods. It also supports the
definition of observations that can be made of the state of program objects and the incorporation of those observations as
predicates that can be instantiated in the scope of object quantifiers and used in describing common forms of state/event
sequencing properties. We illustrate how BSL can be used to formulate a variety of system correctness properties for several
multi-threaded Java applications.
Published online: 2 October 2002 相似文献
7.
This paper presents an approach for the automated debugging of reactive and concurrent Java programs, combining model checking and runtime monitoring. Runtime monitoring is used to transform the Java execution traces into the input for the model checker, the purpose of which is twofold. First, it checks these execution traces against properties written in linear temporal logic (LTL), which represent desirable or undesirable behaviors. Second, it produces several execution traces for a single Java program by generating test inputs and exploring different schedulings in multithreaded programs. As state explosion is the main drawback to model checking, we propose two abstraction approaches to reduce the memory requirements when storing Java states. We also present the formal framework to clarify which kinds of LTL safety and liveness formulas can be correctly analysed with each abstraction for both finite and infinite program executions. A major advantage of our approach comes from the model checker, which stores the trace of each failed execution, allowing the programmer to replay these executions to locate the bugs. Our current implementation, the tool TJT, uses Spin as the model checker and the Java Debug Interface (JDI) for runtime monitoring. TJT is presented as an Eclipse plug-in and it has been successfully applied to debug complex public Java programs. 相似文献
8.
Theo C. Ruys Ed Brinksma 《International Journal on Software Tools for Technology Transfer (STTT)》2003,4(2):246-259
In this paper we take a closer look at the automated analysis of designs, in particular of verification by model checking.
Model checking tools are increasingly being used for the verification of real-life systems in an industrial context. In addition
to ongoing research aimed at curbing the complexity of dealing with the inherent state space explosion problem – which allows
us to apply these techniques to ever larger systems – attention must now also be paid to the methodology of model checking,
to decide how to use these techniques to their best advantage. Model checking “in the large” causes a substantial proliferation
of interrelated models and model checking sessions that must be carefully managed in order to control the overall verification
process. We show that in order to do this well both notational and tool support are required. We discuss the use of software
configuration management techniques and tools to manage and control the verification trajectory. We present Xspin/Project,
an extension to Xspin, which automatically controls and manages the validation trajectory when using the model checker Spin.
Published online: 18 June 2002 相似文献
9.
A minimized automaton representation of reachable states 总被引:1,自引:0,他引:1
Gerard J. Holzmann Anuj Puri 《International Journal on Software Tools for Technology Transfer (STTT)》1999,2(3):270-278
We consider the problem of storing a set S⊂Σkas a deterministic finite automaton (DFA). We show that inserting a new string σ∈Σk or deleting a string from the set S represented as a minimized DFA can be done in expected time O(k|Σ|), while preserving
the minimality of the DFA. The method can be applied to reduce the memory requirements of model checkers that are based on
explicit state enumeration. As an example, we discuss an implementation of the method for the model checker Spin. 相似文献
10.
Rafael H. Bordini Michael Fisher Willem Visser Michael Wooldridge 《Autonomous Agents and Multi-Agent Systems》2006,12(2):239-256
This paper gives an overview of our recent work on an approach to verifying multi-agent programs. We automatically translate
multi-agent systems programmed in the logic-based agent-oriented programming language AgentSpeak into either Promela or Java,
and then use the associated Spin and JPF model checkers to verify the resulting systems. We also describe the simplified BDI
logical language that is used to write the properties we want the systems to satisfy. The approach is illustrated by means
of a simple case study. 相似文献
11.
Web应用的快速发展及其一些异于传统程序的特点使Web应用的验证面临了新的挑战。使用接口自动机对Web应用的构件和构件组合进行行为建模,设计了接口自动机到模型检验器Spin程序的转换算法,然后利用Spin检验Web应用的性质,通过一个简单的网上银行示例说明了整个验证过程。 相似文献
12.
In design by contract (DBC), assertions are typically written using program variables and query methods. The lack of separation between program code and assertions is confusing, because readers do not know what code is intended for use in the program and what code is only intended for specification purposes. This lack of separation also creates a potential runtime performance penalty, even when runtime assertion checks are disabled, due to both the increased memory footprint of the program and the execution of code maintaining that part of the program's state intended for use in specifications. To solve these problems, we present a new way of writing and checking DBC assertions without directly referring to concrete program states, using ‘model’, i.e. specification‐only, variables and methods. The use of model variables and methods does not incur the problems mentioned above, but it also allow one to write more easily assertions that are abstract, concise, and independent of representation details, and hence more readable and maintainable. We implemented these features in the runtime assertion checker for the Java Modeling Language (JML), but the approach could also be implemented in other DBC tools. Copyright © 2005 John Wiley & Sons, Ltd. 相似文献
13.
14.
15.
模型检测技术已成功地运用于验证复杂系统的性质。本文提出运用Promela语言对电子商务协议进行建模的方法,对比分析了有无入侵者时简化的SET协议的运行情况。运用Spin模型检测工具,对SET协议的Promela模型进行了检测,对电子商务协议中的关键性质认证性和保密性进行了分析与检测,发现了协议中的缺陷。 相似文献
16.
17.
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. 相似文献
18.
Saswat Anand Corina S. Păsăreanu Willem Visser 《International Journal on Software Tools for Technology Transfer (STTT)》2009,11(1):53-67
We address the problem of error detection for programs that take recursive data structures and arrays as input. Previously
we proposed a combination of symbolic execution and model checking for the analysis of such programs: we put a bound on the size of the program inputs and/or the search depth of the model checker to limit the search state space. Here we look
beyond bounded model checking and consider state matching techniques to limit the state space. We describe a method for examining
whether a symbolic state that arises during symbolic execution is subsumed by another symbolic state. Since the number of symbolic states may be infinite, subsumption is not enough to ensure termination.
Therefore, we also consider abstraction techniques for computing and storing abstract states during symbolic execution. Subsumption
checking determines whether an abstract state is being revisited, in which case the model checker backtracks—this enables
analysis of an under-approximation of the program behaviors. We illustrate the technique with abstractions for lists and arrays. We also discuss abstractions
for more general data structures. The abstractions encode both the shape of the program heap and the constraints on numeric
data. We have implemented the techniques in the Java PathFinder tool and we show their effectiveness on Java programs. This
paper is an extended version of Anand et al. (Proceedings of SPIN, pp. 163–181, 2006). 相似文献
19.
This paper shows how to integrate two complementary techniques for manipulating program invariants: dynamic detection and static verification. Dynamic detection proposes likely invariants based on program executions, but the resulting properties are not guaranteed to be true over all possible executions. Static verification checks that properties are always true, but it can be difficult and tedious to select a goal and to annotate programs for input to a static checker. Combining these techniques overcomes the weaknesses of each: dynamically detected invariants can annotate a program or provide goals for static verification, and static verification can confirm properties proposed by a dynamic tool.We have integrated a tool for dynamically detecting likely program invariants, Daikon, with a tool for statically verifying program properties, ESC/Java. Daikon examines run-time values of program variables; it looks for patterns and relationships in those values, and it reports properties that are never falsified during test runs and that satisfy certain other conditions, such as being statistically justified. ESC/Java takes as input a Java program annotated with preconditions, postconditions, and other assertions, and it reports which annotations cannot be statically verified and also warns of potential runtime errors, such as null dereferences and out-of-bounds array indices.Our prototype system runs Daikon, inserts its output into code as ESC/Java annotations, and then runs ESC/Java, which reports unverifiable annotations. The entire process is completely automatic, though users may provide guidance in order to improve results if desired. In preliminary experiments, ESC/Java verified all or most of the invariants proposed by Daikon. 相似文献