
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Stefan Andrei, Wei Ngan Chin, Albert Mo Kim Cheng, Mihai Lupu, "Automatic Debugging of RealTime Systems Based on Incremental Satisfiability Counting," IEEE Transactions on Computers, vol. 55, no. 7, pp. 830842, July, 2006.  
BibTex  x  
@article{ 10.1109/TC.2006.97, author = {Stefan Andrei and Wei Ngan Chin and Albert Mo Kim Cheng and Mihai Lupu}, title = {Automatic Debugging of RealTime Systems Based on Incremental Satisfiability Counting}, journal ={IEEE Transactions on Computers}, volume = {55}, number = {7}, issn = {00189340}, year = {2006}, pages = {830842}, doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2006.97}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Automatic Debugging of RealTime Systems Based on Incremental Satisfiability Counting IS  7 SN  00189340 SP830 EP842 EPD  830842 A1  Stefan Andrei, A1  Wei Ngan Chin, A1  Albert Mo Kim Cheng, A1  Mihai Lupu, PY  2006 KW  Realtime system KW  system development tools KW  automatic debugging KW  formal methods KW  timing constraint KW  counting SAT problem KW  incremental computation. VL  55 JA  IEEE Transactions on Computers ER   
[1] S. Andrei, W.N. Chin, A. Cheng, and M. Lupu, “Systematic Debugging of RealTime Systems Based on Incremental Satisfiability Counting,” Proc. 11th IEEE RealTime and Embedded Technology and Applications Symp., pp. 519528, 2005.
[2] F. Jahanian and A. Mok, “Safety Analysis of Timing Properties in RealTime Systems,” IEEE Trans. Software Eng., vol. 12, no. 9, pp. 890904, Sept. 1986.
[3] F. Jahanian and A. Mok, “A GraphTheoretic Approach for Timing Analysis and Its Implementation,” IEEE Trans. Computers, vol. 36, no. 8, pp. 961975, Aug. 1987.
[4] F. Wang and A.K. Mok, “RTL and Refutation by Positive Cycles,” Proc. Formal Methods Europe Symp., pp. 659680, 1994.
[5] S. Andrei and W.N. Chin, “Incremental Satisfiability Counting for RealTime Systems,” Proc. 10th IEEE RealTime and Embedded Technology and Applications Symp., pp. 482489, 2004.
[6] A. Mok, private communication, Mar. 2005.
[7] F. Jahanian and D.A. Stuart, “A Method for Verifying Properties of Modechart Specifications,” Proc. Ninth IEEE RealTime Systems Symp., pp. 1221, 1988.
[8] A.M.K. Cheng, RealTime Systems. Scheduling, Analysis, and Verification. WileyInterscience, 2002.
[9] “SDRTL: Systematic Debugging for Path RealTime Logic,” technical report, School of Computing, Nat'l Univ. of Singapore, May 2004, http://www.comp.nus.edu.sg/~andreiSDRTL.
[10] B. Zupan and A.M.K. Cheng, “Optimization of RuleBased Systems Using State Space Graphs,” IEEE Trans. Knowledge and Data Eng., vol. 10, no. 2, pp. 238254, Mar./Apr. 1998.
[11] S. Sodhi and A.M.K. Cheng, “Optimizing Timing Analysis and Verification of Embedded Systems Using RuleBasedAnalytic Techniques,” Proc. WIP Session of IEEECS RealTime Systems Symp., 2003.
[12] A. Dasdan, “Efficient Algorithms for Debugging Timing Constraint Violations,” Proc. Eighth ACM/IEEE Int'l Workshop Timing Issues in the Specification and Synthesis of Digital Systems, pp. 5056, 2002.
[13] A.K. Mok, D.C. Tsou, and R.C.M. de Rooij, “The MSP. RTL RealTime Scheduler Synthesis Tool,” Proc. 17th IEEE RealTime Systems Symp., pp. 118128, 1996
[14] L.E.P. Rice and A.M.K. Cheng, “Timing Analysis of the X38 Space Station Crew Return Vehicle Avionics,” Proc. Fifth IEEECS RealTime Technology and Applications Symp., pp. 255264, 1999.
[15] J.N. Hooker, “Solving the Incremental Satisfiability Problem,” J. Logic Programming, vol. 15, pp. 177186, 1993.
[16] M. Davis, G. Logemann, and D. Loveland, “A Machine Program for TheoremProving,” Comm. ACM, vol. 5, pp. 394397, 1962.
[17] J. Whittemore, J. Kim, and K. Sakallah, “SATIRE: A New Incremental Satisfiability Engine,” Proc. 38th ACM/IEEE Conf. Design Automation, pp. 542545, 2001.
[18] S. Andrei, “The Determinant of the Boolean Formulae,” Analele Universitaţii Bucureşti, Informatica, vol. XLIV, pp. 8392, 1995.
[19] S. Andrei, “Counting for Satisfiability by Inverting Resolution,” Artificial Intelligence Rev., vol. 22, no. 4, pp. 339366, 2004.
[20] J.C. Tiernan, “An Efficient Search Algorithm to Find the Elementary Circuits of a Graph,” Comm. ACM, vol. 13, no. 12, pp. 722726, 1970.
[21] R. Washington, “OnBoard RealTime State and Fault Identification for Rovers,” Proc. IEEE Int'l Conf. Robotics and Automation, pp. 11751181, 2000.
[22] R. Volpe, I. Nesnas, T. Estlin, D. Mutz, R. Petras, and H. Das, “The CLARAty Architecture for Robotic Autonomy,” Proc. 2001 IEEE Aerospace Conf., pp. 121132, 2001.
[23] S. Bayraktar, G.E. Fainekos, and G.J. Pappas, “Experimental Cooperative Control of FixedWing Unmanned Aerial Vehicles,” Proc. 43rd IEEE Conf. Decision and Control, pp. 42924298, 2004.
[24] D. Roth, “On the Hardness of Approximate Reasoning,” Artificial Intelligence, vol. 82, pp. 273302, 1996.
[25] E.M. Clarke and E.A. Emerson, “Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic,” Proc. IBM Workshop Logics of Programs, pp. 5271, 1981.
[26] E.M. Clarke, E.A. Emerson, and A.P. Sistla, “Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach,” ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244263, 1986.
[27] R.E. Bryant, “GraphBased Algorithms for Boolean Function Manipulation,” IEEE Trans. Computers, vol. 35, no. 8, pp. 677691, Aug. 1986.
[28] J.R. Burch, E.M. Clarke, and K.L. McMillan, “Symbolic Model Checking: $10^{20}$ States and Beyond,” Information and Computation, vol. 98, no. 2, pp. 142170, 1992.
[29] K.L. McMillan, Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic, 1993.
[30] A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu, “Symbolic Model Checking without BDDs,” Proc. Fifth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 193207, 1999.
[31] A. Biere, A. Cimatti, E.M. Clarke, M. Fujita, and Y. Zhu, “Symbolic Model Checking Using SAT Procedures Instead of BDDs,” Proc. 36th ACM/IEEE Conf. Design Automation, pp. 317320, 1999.
[32] S. Andrei and W.N. Chin, “Incremental Satisfiability Counting for RealTime Systems,” Technical Report TR0304, Faculty of Computer Science, Iaşi University, România, Sept. 2003, http://www.infoiasi.ro/trtr.pl.cgi.
[33] A. Bouajjani, S. Tripakis, and S. Yovine, “OntheFly Symbolic Model Checking for RealTime Systems,” Proc. 18th IEEE RealTime Systems Symp., pp. 2534, 1997.
[34] A.M.K. Cheng and S. Fujii, “SelfStabilizing RealTime OPS5 Production Systems,” IEEE Trans. Knowledge and Data Eng., vol. 16, no. 12, pp. 15431554, Dec. 2004.
[35] K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi, “Efficient Verification of RealTime Systems: Compact Data Structure and StateSpace Reduction,” Proc. 18th IEEE RealTime Systems Symp., pp. 1424, 1997.
[36] K.G. Larsen, P. Pettersson, and W. Yi, “UPPAAL: Status and Developments,” Proc. Ninth Int'l Conf. Computer Aided Verification, O. Grumberg, ed., pp. 456459, 1997.
[37] F. Jahanian and A. Mok, “Modechart: A Specification for RealTime Systems,” IEEE Trans. Software Eng., vol. 20, no. 12, pp. 933947, Dec. 1994.
[38] D.A. Stuart, M. Brockmeyer, A.K. Mok, and F. Jahanian, “SimulationVerification: Biting at the State Explosion Problem,” IEEE Trans. Software Eng., vol. 27, no. 7, pp. 599617, July 2001.
[39] L.R. Welch, B. Ravindran, B.A. Shirazi, and C. Bruggeman, “Specification and Modeling of Dynamic, Distributed RealTime Systems,” Proc. IEEE RealTime Systems Symp., pp. 7281, 1998.