Titlebook: Rigorous Development of Complex Fault-Tolerant Systems; Michael Butler,Cliff B. Jones,Elena Troubitsyna Book 2006 Springer-Verlag Berlin H

跳脱衣舞的人

0302-9743 faults appearing that cannot be traced back easily to the code. Some of these "faults" could also be unexpected program behavior that appears as a result of interactions between different parts of the program; this is commonly known as complexity. New methods, approaches, tools and techniques are ne

小卒

Book 2006earing that cannot be traced back easily to the code. Some of these "faults" could also be unexpected program behavior that appears as a result of interactions between different parts of the program; this is commonly known as complexity. New methods, approaches, tools and techniques are needed to co

Acquired

Intuitive

Formal Service-Oriented Development of Fault Tolerant Communicating SystemsUML2. We formalize Lyra in the B Method by proposing a set of formal specification and refinement patterns reflecting the essential models and transformations of the Lyra service specification, decomposition and distribution phases. Moreover, we extend Lyra to integrate reasoning about fault tolerance in the entire development flow.

监禁

Formal Analysis of the Operational Concept for the Small Aircraft Transportation Systemmplies with a set of safety requirements such as absence of dead-locks, maintaining aircraft separation, and robustness with respect to the occurrence of off-nominal events. The models also serve as design tools. Indeed, they were used to configure the nominal flight procedures and the geometry of the SATS airspace.

Hdl348

strain

Ophthalmoscope

Are Practitioners Writing Contracts?rical study measuring the proportion of assertion statements used in Eiffel contracts. The study results indicate that programmers using Eiffel (the only active language with built-in support for DBC) tend to write assertions in a proportion that is higher than for other languages.

独特性

废止

On Specification and Verification of Location-Based Fault Tolerant Mobile Systems the state space explosion. The model checking technique adopted in our work is partial order model checking based on Petri net unfoldings, and we use a semantics preserving translation from the process terms used in the modelling of . to a suitable class of high-level Petri nets.