| Summary: | <p>In this dissertation, the concept of using domain specific language to develop error-free
parallel asynchronous load scheduling protocols for distributed systems is studied. The
motivation of this study is rooted in addressing the high cost of verifying parallel asynchronous
load scheduling protocols. Asynchronous parallel applications are prone to subtle
bugs such as deadlocks and race conditions due to the possibility of non-determinism.
Due to this non-deterministic behavior, traditional testing methods are less effective at
finding software faults. One approach that can eliminate these software bugs is to employ
model checking techniques that can verify that non-determinism will not cause software
faults in parallel programs. Unfortunately, model checking requires the development of
a verification model of a program in a separate verification language which can be an
error-prone procedure and may not properly represent the semantics of the original system.
The model checking approach can provide true positive result if the semantics of
an implementation code and a verification model is represented under a single framework
such that the verification model closely represents the implementation and the automation
of a verification process is natural. In this dissertation, a domain specific language
based verification framework is developed to design parallel load scheduling protocols and
automatically verify their behavioral properties through model checking. A specification
language, LBDSL, is introduced that facilitates the development of parallel load scheduling
protocols. The LBDSL verification framework uses model checking techniques to verify
the asynchronous behavior of the protocol. It allows the same protocol specification to be
used for verification and the code generation. The support to automatic verification during
protocol development reduces the verification cost post development. The applicability of
LBDSL verification framework is illustrated by performing case study on three different
types of load scheduling protocols. The study shows that the LBDSL based verification
approach removes the need of debugging for deadlocks and race bugs which has potential
to significantly lower software development costs.</p>
|
|---|
