Compositional verification of fault-tolerant real-time programs

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Compositional verification of fault-tolerant real-time programs

Full text

Pdf (427 KB)

Source

International Conference on Compilers, Architecture and Synthesis for Embedded Systems archive
Proceedings of the seventh ACM international conference on Embedded software table of contents

Grenoble, France

SESSION: Analysis and verification table of contents

Pages 29-38

Year of Publication: 2009

ISBN:978-1-60558-627-4

Authors

Borzoo Bonakdarpour	VERIMAG, Grenoble, France
Sandeep S. Kulkarni	Michigan State University, East Lansing, MI, USA

Sponsors

ACM: Association for Computing Machinery
SIGBED: ACM Special Interest Group on Embedded Systems
SIGMICRO: ACM Special Interest Group on Microarchitectural Research and Processing
SIGDA: ACM Special Interest Group on Design Automation

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 22, Downloads (12 Months): 22, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1629335.1629341 What is a DOI?

ABSTRACT

A hard-masking real-time program is one that satisfies safety (including timing constraints) and liveness properties in the absence and presence of faults. It has been shown that any hard-masking program can be decomposed into a fault-intolerant version and a set of fault-tolerance components known as detectors and delta-correctors. In this paper, we introduce a set of sufficient conditions for interference-freedom among fault-tolerance components and real-time programs. We demonstrate that such conditions elegantly enable us to compositionally verify the correctness of hard-masking programs. Preliminary model checking experiments show very encouraging results in both achieving speedups and reducing memory usage in verification of embedded systems.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	M. Abadi and L. Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(1):73--132, Jan. 1993.
	2	M. Abadi and L. Lamport. Conjoining specifications. ACM Transactions on Programming Languages and Systems (TOPLAS), 17(3):507--534, May 1995.
	3	B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters, 21:181--185, 1985.
	4	R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183--235, 1994.
	5	R. Alur and T. A. Henzinger. Real-time system = discrete system + clock variables. International Journal on Software Tools for Technology Transfer, 1(1-2):86--109, 1997.
	6	R. Alur and T. A. Henzinger. Reactive modules. Formal Methods in System Design, 15(1):7--48, 1999.
	7	A. Arora and S. S. Kulkarni. Detectors and correctors: A theory of fault-tolerance components. In International Conference on Distributed Computing Systems (ICDCS), pages 436--443, 1998.
	8	B. Bonakdarpour and S. S. Kulkarni. Incremental synthesis of fault-tolerant real-time programs. In International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS), LNCS 4280, pages 122--136, 2006.
	9	B. Bonakdarpour and S. S. Kulkarni. Masking faults while providing bounded-time phased recovery. In International Symposium on Formal Methods (FM), pages 374--389, 2008.
	10	B. Bonakdarpour, S. S. Kulkarni, and A. Arora. Disassembling real-time fault-tolerant programs. In ACM International Conference on Embedded Software (EMSOFT), pages 169--178, 2008.
	11	E. M. Clarke, D. E. Long, and K. L. McMillan. Compositional model checking. In Logic in Computer Science (LICS), pages 353--362, 1989.
	12	J. M. Cobleigh, G. S. Avrunin, and L. A. Clarke. Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning. ACM Transactions on Software Engineering and Methodology (TOSEM), 17(2), 2008.
	13	E. W. Dijkstra. Self-stabilizing systems in spite of distributed control. Communications of the ACM, 17(11), 1974.
	14	S. Ghosh and X. He. Fault--containing self-stabilization using priority scheduling. Information Processing Letters, 73(3-4):145--151, 2000.
	15	O. Grumberg and D. E. Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems (TOPLAS), 16(3):843--871, 1994.
	16	T. A. Henzinger. Sooner is safer than later. Information Processing Letters, 43(3):135--141, 1992.
	17	R. D. Jeffords, C. L. Heitmeyer, and M. Archer. Adding fault-tolerance to requirements specifications. Under review - Personal communication, 2007.
	18	A. Jhumka, F. Gartner, C. Fetzer, and N. Suri. On systematic design of fast and perfect detectors. Technical Report 200263, School of Computer and Communication Sciences, EPFL, 2002.
	19	S. S. Kulkarni and A. Ebnenasir. Automated synthesis of multitolerance. In International Conference on Dependable Systems and Networks (DSN), pages 209--219, 2004.
	20	S. S. Kulkarni, J. Rushby, and N. Shankar. A case-study in component-based mechanical verification of fault-tolerant programs. In Internationa Workshop on Self-Stabilization (WSS), pages 33--40, June 1999.
	21	K. G. Larsen, P. Pattersson, and W. Yi. UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer, 1(1-2):134--152, 1997.
	22	J. Rushby. An overview of formal verification for the time-triggered architecture. In Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT), pages 83--105, 2002.
	23	E. W. Stark. A proof technique for rely/guarantee properties. In Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pages 369--391, 1985.
	24	O. Theel and F. Gartner. An exercise in proving convergence through transfer functions. In Workshop on Self-Stabilizing Systems (SSS), pages 41--47, 1999.