References of "Formal Methods in System Design"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailModel-based verification of a security protocol for conditional access to services
Leduc, Guy ULg; Bonaventure, Olivier; Koerner, Eckhart et al

in Formal Methods In System Design (1999), 14(2), 171-191

We use the formal language LOTOS to specify and verify the robustness of the Equicrypt protocol under design in the European OKAPI project for conditional access to multimedia services. We state some ... [more ▼]

We use the formal language LOTOS to specify and verify the robustness of the Equicrypt protocol under design in the European OKAPI project for conditional access to multimedia services. We state some desired security properties and formalize them. We describe a generic intruder process and its modelling, and show that some properties are falsified in the presence of this intruder. The diagnostic sequences can be used almost directly to exhibit the scenarios of possible attacks on the protocol. Finally, we propose an improvement of the protocol which satisfies our properties. [less ▲]

Detailed reference viewed: 10 (0 ULg)
Full Text
Peer Reviewed
See detailSymbolic Verification of Communication Protocols with Infinite State Spaces using QDDs
Boigelot, Bernard ULg; Godefroid, Patrice

in Formal Methods in System Design (1999), 14(3), 237-255

We study the verification of properties of communication protocols modeled by a finite set of finite-state machines that communicate by exchanging messages via unbounded FIFO queues. It is well-known that ... [more ▼]

We study the verification of properties of communication protocols modeled by a finite set of finite-state machines that communicate by exchanging messages via unbounded FIFO queues. It is well-known that most interesting verification problems, such as deadlock detection, are undecidable for this class of systems. However, in practice, these verification problems may very well turn out to be decidable for a subclass containing most "real" protocols. Motivated by this optimistic (and, we claim, realistic) observation, we present an algorithm that may construct a finite and exact representation of the state space of a communication protocol, even if this state space is infinite. Our algorithm performs a loop-first search in the state space of the protocol being analyzed. A loop-first search is a search technique that attempts to explore first the results of successive executions of loops in the protocol description (code). A new data structure named Queue-content Decision Diagram (QDD) is introduced for representing (possibly infinite) sets of queue-contents. Operations for manipulating QDDs during a loop-first search are presented. A loop-first search using QDDs has been implemented, and experiments on several communication protocols with infinite state spaces have been performed. For these examples, our tool completed its search, and produced a finite symbolic representation for these infinite state spaces. [less ▲]

Detailed reference viewed: 9 (1 ULg)
Peer Reviewed
See detailUsing Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties
Godefroid, Patrice; Wolper, Pierre ULg

in Formal Methods in System Design (1993), 2(2), 149--164

This article presents an algorithm for detecting deadlocks in concurrent finite-state systems without incurring most of the state explosion due to the modeling of concurrency by interleaving. For systems ... [more ▼]

This article presents an algorithm for detecting deadlocks in concurrent finite-state systems without incurring most of the state explosion due to the modeling of concurrency by interleaving. For systems that have a high level of concurrency, our algorithm can be much more efficient than the classical exploration of the whole state space. Finally, we show that our algorithm can also be used for verifying arbitrary safety properties. [less ▲]

Detailed reference viewed: 13 (0 ULg)
Peer Reviewed
See detailMemory Efficient Algorithms for the Verification of Temporal Properties
Courcoubetis, Constantin; Vardi, Moshe Y; Wolper, Pierre ULg et al

in Formal Methods in System Design (1992), 1

Detailed reference viewed: 12 (0 ULg)