Biomedical Engineering Reference
In-Depth Information
tool, model checker tool, real-time animator, and finally generates the source code
using the automatic tools. System development process is concurrently assessed by
safety assessment approach [ 11 ] to comply with certification standards. Applying
these new approaches for highly critical systems have many benefits, i.e. the expo-
sure of errors, which might not have been detected without formal methods. The
guidance of NITRD [ 6 ] allows adoption of formal methods into an established set
of processes for development and verification of a high confidence medical device
to be an evolutionary refinement rather than an abrupt change of methodology.
11.3 Techniques and Tools
The topic work also advances the development of new techniques and tools for
supporting the new life-cycle methodology, and is explained in subsequent phases:
Real time animator is used to validate the formal model with real-time data set
at an early stage of system development without generating the source code [ 15 ],
and to bridge the gap between software engineers and stakeholders to build quality
system and discover all ambiguous informations from the requirements. The com-
bined approach of formal verification and real-time animation allows the systematic
development of a clear, concise, precise and unambiguous specification of a soft-
ware system and enables software engineers to animate the formal specification at
an early stage of the development. Moreover, there are scientific and legal applica-
tions as well, where the formal model based animation can be used to simulate (or
emulate) certain scenarios to glean more information or better understandings of the
system to improve the final given system.
Another significant contribution towards improving techniques and tools section
is the “refinement chart”, which is used to present the whole system using layer-
ing approach in graphical block diagrams, where functional blocks are divided into
multiple simpler blocks in a new refinement level, without changing the original
behaviour of the system. The refinement chart offers a clear view of assistance in
“system” integration. This approach also gives a clear view about the system assem-
bling based on operating modes and different kinds of features. This is an important
issue not only for being able to derive system-level performance and correctness
guarantees, but also for being able to assemble components in a cost-effective man-
ner. The complexity of design is reduced by structuring systems using modes and
by detailing this design using refinement.
Automatic code generation from a proved formal model to the target program-
ming language is an essential step for system implementation, which is an equally
important contribution. We have developed the main principles, rules, and imple-
mentation solutions for the translation tool, and also code verification techniques
for generating target programming language (C, C++, Java and C#) code satisfying
Event-B specifications [ 3 , 14 , 16 , 17 ]. The syntax adopted is restrictive, but with
many salient and essential characteristics for the most numeric applications, sup-
ports powerful static-analysis methods and generates fast and safe source code in
Search WWH ::




Custom Search