Título
A methodology for model-based verification of safety contracts and performance requirementsOtras instituciones
Universidad Politécnica de Madrid (UPM)Universidad de Zaragoza
Versión
Postprint
Derechos
© 2018 SAGE PublicationsAcceso
Acceso abiertoVersión del editor
https://doi.org/10.1177/1748006X16667328Publicado en
Journal of Risk and Reliability: Proceedings of the Institution of Mechanical Engineers, Part O Vol. 232. Nº3. Pp. 227-247. June, 2018Primera página
227Última página
247Editor
SAGEPalabras clave
Safety analysis
rail system safety
performance modelling
modelling/simulation ... [+]
rail system safety
performance modelling
modelling/simulation ... [+]
Safety analysis
rail system safety
performance modelling
modelling/simulation
life cycle engineering [-]
rail system safety
performance modelling
modelling/simulation
life cycle engineering [-]
Resumen
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 r ... [+]
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. [-]
Sponsorship
Comisión EuropeaID Proyecto
.Colecciones
- Artículos - Ingeniería [639]