28532 articles – 22057 references  [version française]

inria-00637756, version 1

Formal Specification of Medical Systems by Proof-Based Refinement

Dominique Méry () 1, Neeraj Kumar Singh () a, 1

ACM Transactions in Embedded Computing Systems (TECS) (2012)

Abstract: Formal methods have emerged as an alternative approach to ensuring quality and correctness of highly critical systems, overcoming limitations of traditional validation techniques such as simulation and testing. We propose a refinement-based methodology for complex medical systems design, which possesses all the required key features. A refinement-based combined approach of formal verification, model validation using a model-checker and refinement chart is proposed in this methodology for designing a high-confidence medical device. Furthermore, we show the effectiveness of this methodology for the design of a cardiac pacemaker system.

  • a –  INRIA
  • 1:  MOSEL (LORIA)
  • INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
  • Domain : Computer Science/Modeling and Simulation
    Computer Science/Formal Languages and Automata Theory
 
  • inria-00637756, version 1
  • http://hal.inria.fr/inria-00637756
  • oai:hal.inria.fr:inria-00637756
  • From: Neeraj Kumar Singh <>
  • Submitted on: Wednesday, 2 November 2011 18:17:24
  • Updated on: Wednesday, 2 November 2011 18:17:24