共查询到20条相似文献,搜索用时 11 毫秒
1.
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. 相似文献
2.
Analysis of a biphase mark protocol with Uppaal and PVS 总被引:1,自引:1,他引:0
The biphase mark protocol is a convention for representing both a string of bits and clock edges in a square wave. The protocol is frequently used for communication at the physical level of the ISO/OSI hierarchy, and is implemented on microcontrollers such as the Intel 82530 Serial Communications Controller. An important property of the protocol is that bit strings of arbitrary length can be transmitted reliably, despite differences in the clock rates of sender and receiver (drift), variations of the clock rates (jitter), and distortion of the signal after generation of an edge. In this article, we show how the protocol can be modelled naturally in terms of timed automata. We use the model checker Uppaal to derive the maximal tolerances on the clock rates, for different instances of the protocol, and to support the general parametric verification that we formalized using the proof assistant PVS. Based on the derived parameter constraints we propose instances of BMP that are correct (at least in our model) but have a faster bit rate than the instances that are commonly implemented in hardware.F.W. Vaandrager was supported by EU IST project IST-2001-35304 Advanced Methods for Timed Systems (AMETIST).lA.L. de Groot was supported by NWO project 612.062.000 Architecture for Structuring the requirements Specification of Embedded Safety-critical Systems (ASSESS). 相似文献
3.
Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol 总被引:1,自引:0,他引:1
The interplay of real time and probability is crucial to the correctness of the IEEE 1394 FireWire root contention protocol.
We present a formal verification of the protocol using probabilistic model checking. Rather than analyse the functional aspects
of the protocol, by asking such questions as ‘Will a leader be elected?’, we focus on the protocol's performance, by asking
the question ‘How certain are we that a leader will be elected sufficiently quickly?’ Probabilistic timed automata are used
to formally model and verify the protocol against properties which require that a leader is elected before a deadline with
a certain probability. We use techniques such as abstraction, reachability analysis and integer-time semantics to aid the
model-checking process, and the efficacy of these techniques is compared.
Received July 2001/Accepted in revised form November 2002
Correspondence and offprint requests to: Marta Kwiatkowska, School of Computer Science, University of Birmingham, Birmingham B15 2TT, UK. Email: M.Z.Kwiatkowska@cs.bham.ac.uk 相似文献
4.
Verifying the IEEE 1394 FireWire Tree Identify Protocol with SMV 总被引:1,自引:0,他引:1
This case study contains a formal verification of the IEEE 1394 FireWire tree identify protocol. Crucial properties of finite
models of the protocol have been validated with state-of-the-art symbolic model checkers. Various optimisation techniques
were applied to verify concrete and generic configurations.
Received September 2001/Accepted in revised form September 2001
Correspondence and offprint requests to: Viktor Schuppan, Computer Systems Institute, ETH Zurich, 8092 Zurich, Switzerland. Email: Viktor.Schuppan@inf.ethz.ch 相似文献
5.
Design and implementation of a vehicle interface protocol using an IEEE 1394 network 总被引:1,自引:0,他引:1
A wide variety of in-vehicle devices such as camera sensors, navigation systems, telematics and communication equipments have been incorporated into a vehicle to realize Intelligent Transport Systems (ITS) applications. Because an efficient standardized network is required, ITS Data Bus (IDB) has been discussed to carry high-speed multimedia data for audio, video and other real-time ITS applications. For connecting devices in a standardized manner, the IDB network has architecture with a gateway called vehicle interface which is located between automaker’s proprietary network and the standardized IDB network. IEEE 1394 (also known as iLink or FireWire), which can transport multimedia data for consumer electronics, is a good candidate for IDB network. In this paper, we analyze the issues for existing AV/C protocol (application layer protocol over IEEE 1394) to comprise the IDB network. In addition, we designed and implemented the vehicle interface protocol as a higher layer of IEEE 1394 to address the AV/C protocol issues for realizing the whole IDB network architecture. 相似文献
6.
Hong Peng Sofiène Tahar Ferhat Khendek 《International Journal on Software Tools for Technology Transfer (STTT)》2003,4(2):234-245
In this paper, we compare and contrast SPIN and VIS, two widely used formal verification tools. In particular, we devote special
attention to the efficiency of these tools for the verification of communications protocols that can be implemented either
in software or hardware. As a basis of our comparison, we formally describe and verify the Asynchronous Transfer Mode Ring
(ATMR) medium access protocol using SPIN and its hardware model using VIS. We believe that this study is of particular interest
as more and more protocols, like ATM protocols, are implemented in hardware to match high-speed requirements.
Published online: 1 March 2002 相似文献
7.
H. Bowman G. Faconti J.-P. Katoen D. Latella M. Massink 《Formal Aspects of Computing》1998,10(5-6):550-575
We present the formal specification and verification of a lip-synchronisation protocol using the real-time model
checker Uppaal. A number of specifications of this protocol can be found in the literature, but this is the first automatic
verification. We take a published specification of the protocol, code it up in the Uppaal timed automata notation and then
verify whether the protocol satisfies the key properties of jitter and skew. The verification reveals some aws in the protocol.
In particular, it shows that for certain sound and video streams the protocol can time-lock before reaching a prescribed error
state. We also discuss our experience with Uppaal, with particular reference to modelling timeouts and to deadlock analysis.
Received March 1998 / Accepted in revised form October 1998 相似文献
8.
Remy Chevallier Emmanuelle Encrenaz-Tiphene Laurent Fribourg Weiwen Xu 《Formal Methods in System Design》2009,34(1):59-81
Using a variant of Clariso-Cortadella’s parametric method for verifying asynchronous circuits, we analyse some crucial timing
behaviors of the architecture of SPSMALL memory, a commercial product of STMicroelectronics. Using the model of parametric
timed automata and model checker HYTECH, we formally derive a set of linear constraints that ensure the correctness of the
response times of the memory. We are also able to infer the constraints characterizing the optimal setup timings of input
signals. We have checked, for two different implementations of this architecture, that the values given by our model match
remarkably with the values obtained by the designer through electrical simulation.
Partially supported by project MEDEA+ Blueberries.
A preliminary version appeared in the Proceedings of 4th International Conference on Formal Modelling and Analysis of Timed
Systems (FORMATS’06), Sept. 2006. 相似文献
9.
KRONOS: a verification tool for real-time systems 总被引:19,自引:1,他引:19
Sergio Yovine 《International Journal on Software Tools for Technology Transfer (STTT)》1997,1(1-2):123-133
10.
Edmund Clarke Somesh Jha Will Marrero 《International Journal on Software Tools for Technology Transfer (STTT)》2003,4(2):173-188
In this paper we explore how partial-order reduction can make the task of verifying security protocols more efficient. These
reduction techniques have been implemented in our tool Brutus. Partial-order reductions have proved very useful in the domain
of model checking reactive systems. These reductions are not directly applicable in our context because of additional complications
caused by tracking knowledge of various agents. We present partial-order reductions in the context of verifying security protocols
and prove their correctness. Experimental results demonstrating the effectiveness of this reduction technique are also presented.
Published online: 24 January 2003 相似文献
11.
Fady Copty Amitai Irron Osnat Weissberg Nathan Kropp Gila Kamhi 《International Journal on Software Tools for Technology Transfer (STTT)》2003,4(3):335-348
In this paper, we emphasize the importance of efficient debugging in formal verification and present capabilities that we
have developed in order to aid debugging in Intel’s Formal Verification Environment. We have given the name “Counter-Example
Wizard” to the bundle of capabilities that we have developed to address the needs of the verification engineer in the context
of counter-example diagnosis and rectification. The novel features of the Counter-Example Wizard are the multi-value counter-example annotation, constraint-based debugging, and multiple counter-example generation mechanisms. Our experience with the verification of real-life Intel designs shows that these capabilities complement one
another and can help the verification engineer diagnose and fix a reported failure. We use real-life verification cases to
illustrate how our system solution can significantly reduce the time spent in the loop of model checking, specification, and
design modification.
Published online: 21 February 2003 相似文献
12.
Conrado Daws Marta Kwiatkowska Gethin Norman 《Electronic Notes in Theoretical Computer Science》2002,66(2)
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 forward 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 the influence of using a biased coin on this minimal probability. 相似文献
13.
14.
15.
Formal Aspects of Computing - The IEEE 1394 Root Contention Protocol is an industrial leader election algorithm for two processes in which probability, real time and parameters play an important... 相似文献
16.
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 相似文献
17.
18.
19.
Marco Devillers David Griffioen Judi Romijn Frits Vaandrager 《Formal Methods in System Design》2000,16(3):307-320
The IEEE 1394 high performance serial multimedia bus protocol allows several components to communicate with each other at high speed. In this paper we present a formal model and verification of a leader election algorithm that forms the core of the tree identify phase of the physical layer of the 1394 protocol.We describe the algorithm formally in the I/O automata model of Lynch and Tuttle, and verify that for an arbitrary tree topology exactly one leader is elected. A large part of our verification has been checked mechanically with PVS, a verification system for higher-order logic. 相似文献
20.
Sérgio Vale Aguiar Campos Edmund Clarke 《International Journal on Software Tools for Technology Transfer (STTT)》1999,2(3):260-269
The task of checking if a computer system satisfies its timing specifications is extremely important. These systems are often
used in critical applications where failure to meet a deadline can have serious or even fatal consequences. This paper presents
an efficient method for performing this verification task. In the proposed method a real-time system is modeled by a state-transition
graph represented by binary decision diagrams. Efficient symbolic algorithms exhaustively explore the state space to determine
whether the system satisfies a given specification. In addition, our approach computes quantitative timing information such
as minimum and maximum time delays between given events. These results provide insight into the behavior of the system and
assist in the determination of its temporal correctness. The technique evaluates how well the system works or how seriously
it fails, as opposed to only whether it works or not. Based on these techniques a verification tool called Verus has been constructed. It has been used in the verification of several industrial real-time systems such as the robotics system
described below. This demonstrates that the method proposed is efficient enough to be used in real-world designs. The examples
verified show how the information produced can assist in designing more efficient and reliable real-time systems. 相似文献