Formal assessment of reliability specifications in embedded cyber-physical systems

详细信息    查看全文

• 作者：Aritra Hazra^a ; ^{aritrah@cse.iitm.ac.in" class="auth_mail" title="E-mail the corresponding author} ; Pallab Dasgupta^b ; ^{pallab@cse.iitkgp.ernet.in" class="auth_mail" title="E-mail the corresponding author} ; Partha Pratim Chakrabarti^b ; ^{ppckak@cse.iitkgp.ernet.in" class="auth_mail" title="E-mail the corresponding author}
• 关键词：Formal methods ; Temporal logic ; Functional reliability ; Fault-tolerant design ; Verification ; Cyber-physical systems ; AND/OR graph search
• 刊名：Journal of Applied Logic
• 出版年：2016
• 出版时间：November 2016
• 年：2016
• 卷：18
• 期：Complete
• 页码：71-104
• 全文大小：779 K

文摘

Reliability has become an integral component of the design intent of embedded cyber-physical systems. Safety-critical embedded systems are designed with specific reliability targets, and design practices include the appropriate allocation of both spatial and temporal redundancies in the implementation to meet such requirements. With increasing complexity of such systems and considering the large number of components in such systems, redundancy allocation requires a formal scientific basis. In this work, we profess the analysis of the redundancy requirement upfront with the objective of making it an integral part of the specification. The underlying problem is one of synthesizing a formal specification with built-in redundancy artifacts, from the formal properties of the error-free system, the error probabilities of the control components, and the reliability target. We believe that upfront formal analysis of redundancy requirements is important in budgeting the resource requirements from a cost versus reliability perspective. Several case-studies from the automotive domain highlight the efficacy of our proposal.