Optimization of Real-Time Systems Timing Specifications
- 1 January 2006
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
Real-time logic (RTL) is useful for the verification of a safety assertion SA with respect to the specification SP of a real-time system. Since the satisfiability problem for RTL is undecidable, there were many efforts to find proper heuristics for proving that SPrarrSA holds. However, none of such heuristics necessarily finds an "optimal implication". After verifying SPrarrSA, and the system implementing SP is deployed, performance changes as a result of power-saving, faulty components, and cost-saving in the processing platform for the tasks specified in SP affect the computation times of the specified tasks. This leads to a different but related SP, which would violate the original SPrarrSA theorem if SA remains the same. It is desirable, therefore, to determine an optimal SP with the slowest possible computation times for its tasks such that the SA is still guaranteed. This is clearly a fundamental issue in the design and implementation of highly dependable real-time/embedded systems. This paper tackles this fundamental issue by describing a new method for relaxing SP and tightening SA such that SPrarrSA is still a theorem. Experimental results show that less than 20% overhead of the running time of the algorithm for the verification of SPrarrSA is needed to find an optimal theoremKeywords
This publication has 11 references indexed in Scilit:
- Improving WCET by applying a WC code-positioning optimizationACM Transactions on Architecture and Code Optimization, 2005
- Systems architecture: the empirical wayPublished by Association for Computing Machinery (ACM) ,2005
- Composable code generation for distributed giottoACM SIGPLAN Notices, 2005
- Schedulability-driven frame packing for multicluster distributed embedded systemsACM Transactions on Embedded Computing Systems, 2005
- Incremental satisfiability counting for real-time systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2004
- The MSP.RTL real-time scheduler synthesis toolPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Hardware/software synthesis of formal specifications in codesign of embedded systemsACM Transactions on Design Automation of Electronic Systems, 2000
- RTL and refutation by positive cyclesLecture Notes in Computer Science, 1994
- A Graph-Theoretic Approach for Timing Analysis and its ImplementationIEEE Transactions on Computers, 1987
- Safety analysis of timing properties in real-time systemsIEEE Transactions on Software Engineering, 1986