by Dominik Dietrich, Lutz Schröder and Ewaryst Schulz
Abstract:
Industrial standards establish technical criteria for various engineering artifacts, materials, or services, with a view to ensuring their functionality, safety, and reliability. We develop a methodology and tools to systematically formalize such standards, in particular their domain specific calculation methods, in order to support the automatic verification of functional properties for concrete physical artifacts. We approach this problem in the setting of the Bremen heterogeneous tool set Hets, which allows for the integrated use of a wide range of generic and custom-made logics. Specifically, we (i) design a domain specific language for the formalization of industrial standards; (ii) formulate a semantics of this language in terms of a translation into the higher-order specification language HasCASL , and (iii) integrate computer algebra systems (CAS) with the Hets framework via a generic CAS-Interface in order to execute explicit and implicit calculations specified in the standard. This enables a wide variety of added-value services based on formal reasoning, including verification of parameterized designs and simplification of standards for particular configurations. We illustrate our approach using the European standard EN 1591, which concerns calculation methods for gasketed flange connections that assure the impermeability and mechanical strength of the flange-bolt-gasket system.
Reference:
Dominik Dietrich, Lutz Schröder and Ewaryst Schulz: Formalizing and Operationalizing Industrial Standards, In Dimitra Giannakopoulou, Fernando Orejas, eds.: Fundamental Approaches to Software Engineering (FASE 2011), Lecture Notes in Computer Science, vol. 6603, pp. 81–95, Springer, 2011. [preprint]
Bibtex Entry:
@InProceedings{DietrichEA11,
author = {Dominik Dietrich and Lutz Schr{\"o}der and Ewaryst Schulz},
title = {Formalizing and Operationalizing Industrial Standards},
year = {2011},
editor = {Dimitra Giannakopoulou and Fernando Orejas},
booktitle = {Fundamental Approaches to Software Engineering (FASE 2011)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6603},
pages = {81-95},
keywords = {Industrial standards formal verification institutions domain specific language computer algebra calculation method},
comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/fm-standards.pdf"> [preprint] </a>},
abstract = { Industrial standards establish technical criteria for various
engineering artifacts, materials, or services, with a view to
ensuring their functionality, safety, and reliability. We develop a
methodology and tools to systematically formalize such standards, in
particular their domain specific calculation methods, in order to
support the automatic verification of functional properties for
concrete physical artifacts. We approach this problem in the
setting of the Bremen heterogeneous tool set Hets, which allows for
the integrated use of a wide range of generic and custom-made
logics. Specifically, we (i) design a domain specific language for
the formalization of industrial standards; (ii) formulate a
semantics of this language in terms of a translation into the
higher-order specification language HasCASL , and (iii) integrate
computer algebra systems (CAS) with the Hets framework via a generic
CAS-Interface in order to execute explicit and implicit calculations
specified in the standard. This enables a wide variety of
added-value services based on formal reasoning, including
verification of parameterized designs and simplification of
standards for particular configurations. We illustrate our approach
using the European standard EN 1591, which concerns calculation
methods for gasketed flange connections that assure the
impermeability and mechanical strength of the flange-bolt-gasket
system.
},
}