Loading...
Please wait, while we are loading the content...
Similar Documents
Modeling and Verification of Safety Critical Systems: A Case Study on Pacemaker
| Content Provider | CiteSeerX |
|---|---|
| Author | Tuan, Luu Anh Chunzheng, Man Tho, Quan Thanh |
| Abstract | Abstract—The pacemaker challenge proposed by Software Quality Research Laboratory is looking for formal methods to produce precise and reliable systems. Safety critical systems like pacemaker need to guarantee important properties (like deadlock-free, safety, etc.), which concern human lives. Formal methods have been applied in designing safety critical systems with verified desirable properties. In this paper, we propose a formal model of pacemaker, modeling its behaviors and its communication with the external environment, using a real-time formalism. Critical properties, such as deadlock freeness and heart rate limits are then verified using the model checker PAT(Process Analysis Toolkit). This work yields a verified formal model of pacemaker systems, which can serve as specification for real pacemaker implementations. Keywords-Pacemaker; PAT; model checking; verification; I. |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Safety Critical System Case Study Formal Method Pacemaker System Deadlock Freeness Process Analysis Toolkit Reliable System Verified Desirable Property Real Pacemaker Implementation Heart Rate Limit Real-time Formalism Verified Formal Model Model Checking Important Property External Environment Pacemaker Challenge Model Checker Pat Software Quality Research Laboratory Formal Model Critical Property |
| Content Type | Text |
