Software Safety and Dependable Systems

Sungdeok (Steve) Cha
Dept of Computer Science and Engineering
Korea University
Seoul, Korea

http://dependable.korea.ac.kr/
1981~1991

1994~2008

2008~

UCI, 1981
KNICS (Korea Nuclear I&C System)
Reactor Protection Software

MIT, 2013

Artificial Heart (HVAD)KNICS Project• Software qualification for digital safety system(2001~2007)

IEEE Software,
May/June 2009

More on KNICS Project• Programmable Logic
Controller(PLC)-based softwaredevelopment– Using function block diagram (FBD) as
the implementation language– “Project environment” to our group• Formal methods were usedwhenever practical– To automate as much analysis as
possible– To reduce human errors– To provide greater safety assurance– Our group’s own decisionOur Approach

Requirements EngieeringRequirements Modeling
Historynode

Function node

TimedHistorynodeRequirements Modeling• Attempted to balance between readability,expressiveness, and analyzability– Preference of stakeholder, in particular the regulatory body,was taken into consideration– Approval experience on Wolsung NPP 2-3-4 shutdown system(1995~1997)

vsRequirements Modeling• Defined notations AND formal semantics• Automated much of requirements analysis– Completeness, consistency, …
– Model checking

SRS Model Checking①SMV input generationfrom NuSCR spec.
NuSCR2SMVtranslator↑②Insert properties←③Model checking
using SMV↓④Verification Result Analysis

FBD Synthesis• Was feasible due to relatively small (andintended) semantic gap

Synthesized FBD was NOT
Optimized• state- and history-dependent nodes posedchallenge

FBD Verification and VIS• Manual optimization of FBD code was inevitable• Used VIS (Verification Interacting withSynthesis) to support subsequent behavioral
equivalence– Defined FBD translation rules into Verilog

Intuitive and Visual Analysis• To help domain experts better understandresults

14

FBD Testing• FBD, based on its data-flow model, posed
particular challenge– Any test case would satisfy 100% coverage with simplisticdefinition• Had to define a customized coverage criteria tosatisfy regulatory requirements

Obama co-author? ;)FBD-customized
coverage criteria• Defined conditions under which specific input
played direct role in determining the output– d-path condition• Defined various coverage criteria under which
various FBD unit testing could be performed– Basic coverage, input condition coverage, complex condition
coverage– Similar to statement coverage, branch coverage, condition
coverage in traditional (procedural) software testing• Developed a tool to automate test casegeneration (Jee et at., STVR, 2014)– Used Yices, an SMT solver developed by SRI International

KNICS Lessons• Be flexible and attentive to stakeholders’ needs– Including regulatory personnel when relevant• “Let them do the work” ;)– Extremely important that SE professionals communicate andwork well with domain experts– It is NEVER as easy as it seems• Do not reinvent wheels. SMV, VIS, Yices, …
• Provide data visualization/interpretation tools• Domain-specific problems can become
interesting SE challenges (e.g., FBD testingcriteria)Hybrid Ventricular Assist Device• Korea Artificial Organ Center (KAOC) project• Animal-tested for 183 days on a calf, exceeding
the FDA regulations on long-term experiment– No anomaly was detected

H-VAD Software• Event-driven architecture– Pumping Rate (PR), Stroke Length (SL), Start / Stop button– 211 probing statements were added• Control logic in ~3,800 LoC in C
– Relatively simple branch conditions

Time Interrupt Function

In-Vitro Testing• Each button waspressed at least once
• All permitted
parameter values
were covered (e.g.,
SL 30~90, default 60)• Stop button waspressed at arbitrary
and random moments

In-Vitro Testing• Tried to force the system to engage inpredefined emergency modes• Achieved 80.6%, 170 out of 211 probes,
coverage

In-Vitro Testing: Results• Found two behavior patterns, previously
unknown to KAOC staff, that appeared
abnormalMotor control variable

Real PR

Target PR

Real PR
Target PR

Animal Testing and H-VADSoftware• Used two 3-months old piglets• 78.7% code coverage (cf 80.6%)– Due to our inability to force/repeat certain test cases without
endangering the test animal’s life

Animal Testing: Results• Could NOT recreate in-vitro testing result

Motorcontrol variable

Emergency mode wastriggered

Real pump rate
Targetpump rate

SL (-) adj.

SL (-) adj.

SL (-) adj.

Animal Testing: Results• Abnormal pumping pattern, off by 7, repeated

NormalAbnormal

H-VAD Lessons• SE techniques, although common sense andtrivial to us, are not always applied in practice• “Live” testing is expensive, difficult, timeconsuming, …
– It is extremely difficult to make credible claims on software
quality in safety-critical setting• “All NEW H-VAD” project could not be launched– Guide hardware design so as to simplify software design andenhance software safety assurance• Dedicated and continuous involvement ofdomain experts are crucial to the success• Safety-Critical Systems Symposium, Feb 2011,Southampton, UK

Conclusions• Interdisciplinary research is important and doable, but difficult• Software engineering can and should play
important roles in software-driven andsoftware-intensive society• Support domain experts to do their work well
– We must learn to work with domain experts