ABSTRACT
Introduction .................................................................................................... 340 Formal methods ............................................................................................. 341
Spacecraft engineering life cycle ............................................................. 343 Modeling language: An AADL dialect ................................................... 344
Nominal behavior ................................................................................. 345 Error behavior ....................................................................................... 348 Fault injections ...................................................................................... 348 Formal semantics .................................................................................. 349 Graphical modeling.............................................................................. 350
V&V analyses with formal methods ........................................................... 350 Properties .................................................................................................... 351 Functional correctness .............................................................................. 353 Safety and dependability assessment ..................................................... 354 Failure detection, isolation, and recovery effectiveness analysis ....................................................................................................... 355 Performability ............................................................................................ 357
Industrial case studies ................................................................................... 357 Satellite subsystem case studies .............................................................. 358
Satellite mode management case study ............................................ 358 Thermal regulation case study ........................................................... 359 Lessons learned ..................................................................................... 360
Satellite platform preliminary design case study ................................. 361 Satellite architecture ............................................................................. 362 Modeling process .................................................................................. 363 From requirements to formal properties ........................................... 365 Validation activities .............................................................................. 367 Lessons learned ..................................................................................... 369
Introduction Verication and validation (V&V) are key processes in the engineering of safety-critical hardware and software systems. They check whether the system under construction or its artifacts meet their requirements and its intended functions. The current industry practices for conducting V&V are rather labor intensive. There are severe concerns on scaling these practices to deal with the ever-growing complexity of systems and in particular of software. The trend is to incorporate the use of formal methods. In particular, automated verication techniques are attractive for supporting more rigorous V&V. Formal methods, however, tend to require a high degree of expertise and specialized know-how. These incur substantial investments before their cost and efciency benets can be reaped.
