
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Ştefan Andrei, Albert Mo Kim Cheng, "Efficient Verification and Optimization of RealTime LogicSpecified Systems," IEEE Transactions on Computers, vol. 58, no. 12, pp. 16401653, December, 2009.  
BibTex  x  
@article{ 10.1109/TC.2009.79, author = {Ştefan Andrei and Albert Mo Kim Cheng}, title = {Efficient Verification and Optimization of RealTime LogicSpecified Systems}, journal ={IEEE Transactions on Computers}, volume = {58}, number = {12}, issn = {00189340}, year = {2009}, pages = {16401653}, doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2009.79}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Computers TI  Efficient Verification and Optimization of RealTime LogicSpecified Systems IS  12 SN  00189340 SP1640 EP1653 EPD  16401653 A1  Ştefan Andrei, A1  Albert Mo Kim Cheng, PY  2009 KW  Realtime system KW  system development tool KW  automatic debugging KW  timing constraint KW  counting SAT problem KW  incremental computation KW  optimization. VL  58 JA  IEEE Transactions on Computers ER   
[1] S. Andrei and A.M.K. Cheng, “Faster Verification of rtlSpecified Systems via Decomposition and Constraint Extension,” Proc. 27th IEEE RealTime Systems Symp., pp. 6776, 2006.
[2] S. Andrei and A.M.K. Cheng, “Optimization of RealTime Systems Timing Specifications,” Proc. 12th IEEE Int'l Conf. Embedded and RealTime Computing Systems and Applications, pp. 6874, 2006.
[3] 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.
[4] 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.
[5] F. Wang and A.K. Mok, “RTL and Refutation by Positive Cycles,” Proc. Formal Methods Europe Symp., pp. 659680, 1994.
[6] F. Jahanian and D.A. Stuart, “A Method for Verifying Properties of Modechart Specifications,” Proc. Ninth IEEE RealTime Systems Symp., pp. 1221, 1988.
[7] 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.
[8] A.M.K. Cheng, RealTime Systems. Scheduling, Analysis, and Verification. Wiley Interscience, 2002.
[9] 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,
[10] 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.
[11] S. Andrei, W.N. Chin, A.M.K. Cheng, and M. Lupu, “Automatic Debugging of RealTime Systems Based on Incremental Satisfiability Counting,” IEEE Trans. Computers, vol. 55, no. 7, pp. 830842, July 2006.
[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] O. Sokolsky and S. Smolka, “Incremental Model Checking in the Modal MuCalculus,” Proc. Int'l Conf. ComputerAided Verification, 1994.
[14] C.L. Conway, K.S. Namjoshi, D. Dams, and S.A. Edwards, “Incremental Algorithms for InterProcedural Analysis of Safety Properties,” Computer Aided Verification, K. Etessami and S.Rajamani, eds., pp. 449461, SpringerVerlag, 2005.
[15] R. Alur, R. Grosu, I. Lee, and O. Sokolsky, “Compositional Refinement for Hierarchical Hybrid Systems,” Proc. Fourth Int'l Workshop Hybrid Systems: Computation and Control, pp. 3348, 2001.
[16] I. Shin and I. Lee, “Compositional RealTime Scheduling Framework,” Proc. RealTime Systems Symp., pp. 5767, 2004.
[17] S.S. Kulkarni, J.M. Rushby, and N. Shankar, “A CaseStudy in ComponentBased Mechanical Verification of FaultTolerant Programs,” Proc. IEEE Int'l Conf. Distributed Computing Systems (ICDCS) Workshop SelfStabilizing Systems, pp. 3340, 1999.
[18] S. Owre, J.M. Rushby, N. Shankar, and D.W.J. StringerCalvert, “PVS: An Experience Report,” Proc. Int'l Workshop Current Trends in Applied Formal Methods—FMTrends '98, pp. 338345, 1998.
[19] G.R. Hellestrand, “Systems Architecture: The Empirical Way: Abstract Architectures to ‘Optimal’ Systems,” Proc. Int'l Conf. Embedded Software, 147158, 2005.
[20] V. Carchiolo, M. Malgeri, and G. Mangioni, “Hardware/Software Synthesis of Formal Specifications in Codesign of Embedded Systems,” Design Automation of Electronic Systems, vol. 5, no. 3, pp.399432, 2000.
[21] W. Zhao, D. Whalley, C. Healy, and F. Mueller, “Improving WCET by Applying a WC Code Positioning Optimization,” ACM Trans. Architecture and Code Optimization, vol. 2, no. 4, pp. 335365, 2005.
[22] T.A. Henzinger, C.M. Kirsch, and S. Matic, “Composable Code Generation for Distributed Giotto,” ACM SIGPLAN Notices, vol. 40, no. 7, pp. 2130, 2005.
[23] P. Pop, P. Eles, and Z. Peng, “SchedulabilityDriven Frame Packing for Multicluster Distributed Embedded Systems,” ACM Trans. Embedded Computing Systems, vol. 4, no. 1, pp.112140, 2005.