Applying Formal Methods into Safety-Critical Health Applications

2014 ◽  
pp. 195-208 ◽  
Author(s):  
Mohammad-Reza Gholami ◽  
Hanifa Boucheneb
Keyword(s):  
Formal Methods ◽  
Safety Critical ◽  
Health Applications

scholarly journals Preface to special issue: lightweight and practical formal methods in the design and analysis of safety-critical systems

2013 ◽  
Vol 23 (4) ◽  
pp. 675-675
Author(s):  
AZER BESTAVROS ◽  
ASSAF KFOURY
Keyword(s):  
Computer Science ◽  
Formal Methods ◽  
Wide Spectrum ◽  
Critical Systems ◽  
Research Groups ◽  
Special Issue ◽  
Mathematical Structures ◽  
Safety Critical ◽  
Safety Critical Systems ◽  
Final Selection

The papers included in this special issue of Mathematical Structures in Computer Science were selected from a larger set we solicited from leading research groups on both sides of the Atlantic. They cover a wide spectrum of tutorials, recent results and surveys in the area of lightweight and practical formal methods in the design and analysis of safety-critical systems. All the papers we received were submitted to a rigorous process of review and revision, based on which we made our final selection.

The practice of formal methods in safety-critical systems

1995 ◽  
Vol 28 (1) ◽  
pp. 77-87 ◽  
Author(s):  
Shaoying Liu ◽  
Victoria Stavridou ◽  
Bruno Dutertre
Keyword(s):  
Formal Methods ◽  
Critical Systems ◽  
Safety Critical ◽  
Safety Critical Systems

scholarly journals Verifiable and Interpretable Reinforcement Learning through Program Synthesis

2019 ◽  
Vol 33 ◽  
pp. 9902-9903
Author(s):  
Abhinav Verma
Keyword(s):  
Neural Network ◽  
Machine Learning ◽  
Neural Networks ◽  
Reinforcement Learning ◽  
Programming Languages ◽  
Formal Methods ◽  
Domain Knowledge ◽  
Policy Search ◽  
Safety Critical ◽  
Symbolic Methods

We study the problem of generating interpretable and verifiable policies for Reinforcement Learning (RL). Unlike the popular Deep Reinforcement Learning (DRL) paradigm, in which the policy is represented by a neural network, the aim of this work is to find policies that can be represented in highlevel programming languages. Such programmatic policies have several benefits, including being more easily interpreted than neural networks, and being amenable to verification by scalable symbolic methods. The generation methods for programmatic policies also provide a mechanism for systematically using domain knowledge for guiding the policy search. The interpretability and verifiability of these policies provides the opportunity to deploy RL based solutions in safety critical environments. This thesis draws on, and extends, work from both the machine learning and formal methods communities.

scholarly journals A methodology for model-based verification of safety contracts and performance requirements

2016 ◽  
Vol 232 (3) ◽  
pp. 227-247 ◽  
Author(s):  
Elena Gómez-Martínez ◽  
Ricardo J Rodríguez ◽  
Clara Benac-Earle ◽  
Leire Etxeberria ◽  
Miren Illarramendi
Keyword(s):  
Formal Methods ◽  
Language Model ◽  
Critical Systems ◽  
Object Constraint Language ◽  
Modelling Language ◽  
Industrial Case Study ◽  
Safety Requirements ◽  
Safety Critical ◽  
Unified Modelling Language ◽  
Constraint Language

The verification of safety requirements becomes crucial in critical systems where human lives depend on their correct functioning. Formal methods have often been advocated as necessary to ensure the reliability of software systems, albeit with a considerable effort. In any case, such an effort is cost-effective when verifying safety-critical systems. Often, safety requirements are expressed using safety contracts, in terms of assumptions and guarantees. To facilitate the adoption of formal methods in the safety-critical software industry, we propose a methodology based on well-known modelling languages such as the unified modelling language and object constraint language. The unified modelling language is used to model the software system while object constraint language is used to express the system safety contracts within the unified modelling language. In the proposed methodology a unified modelling language model enriched with object constraint language constraints is transformed to a Petri net model that enables us to formally verify such safety contracts. The methodology is evaluated on an industrial case study. The proposed approach allows an early safety verification to be performed, which increases the confidence of software engineers while designing the system.

scholarly journals Why Formal Methods Are Considered for Safety Critical Systems?

2015 ◽  
Vol 08 (10) ◽  
pp. 531-538 ◽  
Author(s):  
Monika Singh ◽  
Ashok Kumar Sharma ◽  
Ruhi Saxena
Keyword(s):  
Formal Methods ◽  
Critical Systems ◽  
Safety Critical ◽  
Safety Critical Systems

Practical Formal Methods in Human–Computer Interaction

2018 ◽  
Author(s):  
Alan Dix
Keyword(s):  
Human Computer Interaction ◽  
Computer Science ◽  
Formal Methods ◽  
Case Studies ◽  
Early Development ◽  
Interaction Design ◽  
Formal Training ◽  
Theoretical Interest ◽  
Safety Critical ◽  
Computer Interaction

This chapter explores how precise formal methods can be used effectively and practically in interaction design. The term ‘formal methods’ in computer science refers to a suite of techniques drawing on mathematical notions of sets, logic, and functions or precise diagrammatic notations, most of which are currently primarily focused on safety-critical applications in the aerospace or nuclear industries. While research into broader use of these methods could be regarded as a theoretical interest, the early development of formal methods was driven as much by practical considerations as theory. This chapter features two case studies on formal notations and their use in areas of practical interaction design beyond safety-critical applications, as well as understood, used, and appropriated by clients and designers who have no formal training or expertise. Each offers specific notations and techniques to the reader and also explores more general lessons for creating practical formal methods for HCI.

Sign in / Sign up

Export Citation Format

Share Document