Recent advanced in model-checking have made it practical to
formally verify the correctness of many complex synchronous systems
(i.e., systems driven by a single clock). However, many computer
systems are implemented by asynchronously composing several
synchronous components, where each component has its own clock and
these clocks are not synchronized. Formal verification of such
Globally Asynchronous/Locally Synchronous (GA/LS) architectures is
a much more difficult task. In this report, we describe a
methodology for developing and reasoning about such systems. This
approach allows a developer to start from an ideal system
specification and refine it along two axes. Along one axis, the
system can be refined one component at a time towards an
implementation. Along the other axis, the behavior of the system
can be relaxed to produce a more cost effective but still
acceptable solution. We illustrate this process by applying it to
the synchronization logic of a Dual Fight Guidance System, evolving
the system from an ideal case in which the components do not fail
and communicate synchronously to one in which the components can
fail and communicate asynchronously. For each step, we show how the
system requirements have to change if the system is to be
implemented and prove that each implementation meets the revised
system requirements through modelchecking.
General
Is the information for this product incomplete, wrong or inappropriate?
Let us know about it.
Does this product have an incorrect or missing image?
Send us a new image.
Is this product missing categories?
Add more categories.
Review This Product
No reviews yet - be the first to create one!
Welcome to Loot.co.za!
Sign in / Register |Wishlists & Gift Vouchers |Help | Advanced search
