Jee, Eunkyoung
Email Address
ORCID
Disciplines
Search Results
Now showing 1 - 3 of 3
Publication A Safety-Assured Development Approach for Real-Time Software(2010-08-23) Jee, Eunkyoung; Wang, Shaohui; Kim, Jeong Ki; Lee, Jaewoo; Sokolsky, Oleg; Lee, InsupGuaranteeing timing properties is an important issue as we develop safety-critical real-time systems such as cardiac pacemakers. We present a safety assured development approach of real-time software using a pacemaker as our case study. Following the model-driven development techniques, measurement-based timing analysis is used to guarantee timing properties in implementation as well as in the formal model. Formal specification with timed automata is checked with respect to timing properties by model checking technique and is transformed into implementation systematically. When timing properties may be violated in the implementation due to timing delay, it is suggested to measure the time deviation and reflect it to the code explicitly by modifying guards. The model is altered according to the modifications in the code. These changes of the code and the model are considered safe if all the properties are still satisfied by the modified model in re-performed model hecking. We demonstrate how the suggested approach can be applied to single-threaded and multi-threaded versions of implementation. This approach can provide developers with a useful time-guaranteeing technique applicable to several code generation schemes without imposing many restrictions.Publication Assurance Cases in Model-Driven Development of the Pacemaker Software(2010-10-18) Jee, Eunkyoung; Lee, Insup; Sokolsky, OlegWe discuss the construction of an assurance case for the pace-maker software. The software is developed following a model-based technique that combined formal modeling of the system, systematic code generation from the formal model, and measurement of timing behavior of the implementation. We show how the structure of the assurance case reflects our development approach.Publication Automated Test Coverage Measurement for Reactor Protection System Software implemented in Function Block Diagram(2010-09-14) Jee, Eunkyoung; Kim, Suin; Lee, Insup; Cha, SungdeokWe present FBDTestMeasurer, an automated test coverage measurement tool for function block diagram (FBD) programs which are increasingly used in implementing safety critical systems such as nuclear reactor protection systems. We have defined new structural test coverage criteria for FBD programs in which dataflow-centric characteristics of FBD programs were well reflected. Given an FBD program and a set of test cases, FBDTestMeasurer produces test coverage score and uncovered test requirements with respect to the selected coverage criteria. Visual representation of uncovered data paths enables testers to easily identify which parts of the program need to be tested further. We found many aspects of the FBD logic that were not tested sufficiently when conducting a case study using test cases prepared by domain experts for reactor protection system software. Domain experts found this technique and tool highly intuitive and useful to measure the adequacy of FBD testing and generate additional test cases.