NDLI: Formal hazard analysis of hybrid systems in cTLA

Content Provider	IEEE Xplore Digital Library
Author	Herrmann, P. Krumm, H.
Copyright Year	1999
Description	Author affiliation: Fachbereich Inf., Dortmund Univ., Germany (Herrmann, P.)
Abstract	Hybrid systems like computer-controlled chemical plants are typical safety critical distributed systems. In present practice, the safety of hybrid systems is guaranteed by hazard analysis which is performed according to procedures (e.g., Ha/sub 2/Op) where experts discuss a series of informal argumentations. Each argumentation considers a specific required system property. Formal property proofs can increase the reliability. They, however have often to deal with very complex hybrid systems. Therefore, methods are needed which structure and decompose formal verification tasks into manageable subtasks. With respect to this, our approach achieves a relatively direct translation of informal argumentations into formal proofs. Since the informal argumentations mostly do not refer to the system as a whole but do only address specific parts and aspects, the formal proofs also can deal with partial, less complex system models. In result even very complex systems can be verified in well-manageable subtasks. The direct translation is supported by the characteristics of the specification technique applied. The temporal logic based technique cTLA supports the modular description of hybrid process systems. In particular one can model a system as a composition of behavior constraints. Properties which are implied by a subsystem of constraints also are properties of the system as a whole. Therefore a subsystem can correspond to the parts and aspects addressed by an informal argumentation. We outline cTLA and introduce the formalization of hazard analysis argumentations by means of a hybrid example system. Additionally, we sketch a framework of specification modules and theorems which supports the formal hazard analysis of hybrid systems.
Starting Page	68
Ending Page	77
File Size	208820
Page Count	10
File Format	PDF
ISBN	0769502903
ISSN	10609857
DOI	10.1109/RELDIS.1999.805084
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	1999-10-22
Publisher Place	Switzerland
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Hazards Fault detection Logic Electronic switching systems Electrical capacitance tomography Expert systems Equations Petri nets State-space methods Space exploration
Content Type	Text
Resource Type	Article
Subject	Theoretical Computer Science Computer Networks and Communications Software Hardware and Architecture

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in