Issue No.06 - June (2013 vol.39)
pp: 857-868
G. Rodriguez-Navas , Dept. de Cienc. Mat. i Inf., Univ. de les Illes Balears, Palma de Mallorca, Spain
J. Proenza , Dept. de Cienc. Mat. i Inf., Univ. de les Illes Balears, Palma de Mallorca, Spain
The application of model checking for the formal verification of distributed embedded systems requires the adoption of techniques for realistically modeling the temporal behavior of such systems. This paper discusses how to model with timed automata the different types of relationships that may be found among the computer clocks of a distributed system, namely, ideal clocks, drifting clocks, and synchronized clocks. For each kind of relationship, a suitable modeling pattern is thoroughly described and formally verified.
Real-time systems, Automata, Formal verification, Distributed processing, Embedded systems, hybrid automata, Embedded systems, real-time systems, clock synchronization, model checking, timed automata
G. Rodriguez-Navas, J. Proenza, "Using Timed Automata for Modeling Distributed Systems with Clocks: Challenges and Solutions", IEEE Transactions on Software Engineering, vol.39, no. 6, pp. 857-868, June 2013, doi:10.1109/TSE.2012.73
[1] J.-P. Katoen, Concepts, Algorithms, and Tools for Model Checking. Institut für Mathematische Maschinen und Datenverarbeitung, 1998.
[2] E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking. MIT Press, 2001.
[3] R. Wang, X. Song, and M. Gu, "Modelling and Verification of Program Logic Controllers Using Timed Automata," IET Software, vol. 1, no. 4, pp. 127-131, Aug. 2007.
[4] G.J. Holzmann, R. Joshi, and A. Groce, "Swarm Verification Techniques," IEEE Trans. Software Eng., vol. 37, no. 6, pp. 845-857, Nov./Dec. 2011.
[5] M. Kim, Y. Kim, and H. Kim, "A Comparative Study of Software Model Checkers as Unit Testing Tools: An Industrial Case Study," IEEE Trans. Software Eng., vol. 37, no. 2, pp. 146-160, Mar./Apr. 2011.
[6] E. Brinksma and A. Mader, "On Verification Modelling of Embedded Systems," http://doc.utwente.nl48688/, 2004.
[7] A. Mader, H. Wupper, and M. Boon, "The Construction of Verification Models for Embedded Systems," http://doc. utwente.nl66985/, Jan. 2007.
[8] F. Vaandrager, "QUASIMODO project, Deliverable D3.1: Model Process Improvements," publications.htm , 2010.
[9] R. Alur, C. Courcoubetis, and D. Dill, "Model-Checking in Dense Real-Time," Information and Computation, vol. 104, no. 1, pp. 2-34, 1993.
[10] C. Daws and S. Yovine, "Two Examples of Verification of Multirate Timed Automata with Kronos," Proc. 16th IEEE Real-Time Systems Symp., pp. 66-75, 1995.
[11] G. Behrmann, A. David, and K.G. Larsen, "A Tutorial on Uppaal," Proc. Fourth Int'l School on Formal Methods for the Design of Computer, Comm., and Software Systems, M. Bernardo and F. Corradini, eds., pp. 200-236, Sept. 2004.
[12] H.B. Mokadem, B. Berard, V. Gourcuff, O. De Smet, and J. Roussel, "Verification of a Timed Multitask System with Uppaal," IEEE Trans. Automation Science and Eng., vol. 7, no. 4, pp. 921-932, Oct. 2010.
[13] P. Li, B. Ravindran, S. Suhaib, and S. Feizabadi, "A Formally Verified Application-Level Framework for Real-Time Scheduling on Posix Real-Time Operating Systems," IEEE Trans. Software Eng., vol. 30, no. 9, pp. 613-629, Sept. 2004.
[14] F. Miyawaki, K. Masamune, S. Suzuki, K. Yoshimitsu, and J. Vain, "Scrub Nurse Robot System—Intraoperative Motion Analysis of a Scrub Nurse and Timed-Automata-Based Model for Surgery," IEEE Trans. Industrial Electronics, vol. 52, no. 5, pp. 1227-1235, Oct. 2005.
[15] S. Tschirner, L. Xuedong, and W. Yi, "Model-Based Validation of QoS Properties of Biomedical Sensor Networks," Proc. Seventh ACM Int'l Conf. Embedded Software, 2008.
[16] P. Veríssimo, "Ordering and Timeliness Requirements of Dependable Real-Time Programs," Real-Time Systems, vol. 7, no. 2, pp. 105-128, 1994.
[17] C. Lenzen, T. Locher, and R. Wattenhofer, "Tight Bounds for Clock Synchronization," J. ACM, vol. 57, no. 2,article 8, 2010.
[18] H. Bowman, G. Faconti, J.-P. Katoen, D. Latella, and M. Massink, "Automatic Verification of a Lip-Synchronisation Algorithm Using Uppaal—Extended Version," Proc. Third Int'l Workshop Formal Methods for Industrial Crtical Systems, 1998.
[19] E. Asarin, T. Dang, O. Maler, and O. Bournez, "Approximate Reachability Analysis of Piecewise-Linear Dynamical Systems," Proc. Third Int'l Workshop Hybrid Systems: Computation and Control, pp. 20-31, 2000.
[20] R. Alur, S.L. Torre, and P. Madhusudan, "Perturbed Timed Automata," Proc. Eighth Int'l Workshop Hybrid Systems: Computation and Control, M. Morari and L. Thiele, eds., pp. 70-85, Mar. 2005.
[21] C. Dima and R. Lanotte, "Distributed Time-Asynchronous Automata," Proc. Fourth Int'l Conf. Theoretical Aspects of Computing, pp. 185-200, 2007.
[22] S. Jha, B.A. Brady, and S.A. Seshia, "Symbolic Reachability Analysis of Lazy Linear Hybrid Automata," Proc. Fifth Int'l Conf. Formal Modeling and Analysis of Timed Systems, pp. 241-256, 2007.
[23] S. Mohalik, A. Rajeev, M. Dixit, S. Ramesh, R. Vijay Suman, P. Pandya, and S. Jiang, "Model Checking Based Analysis of End-to-End Latency in Embedded, Real-Time Systems with Clock Drifts," Proc. ACM/IEEE 45th Design Automation Conf., pp. 296-299, June 2008.
[24] M. Wulf, L. Doyen, N. Markey, and J.-F. Raskin, "Robust Safety of Timed Automata," Formal Methods Systems Design, vol. 33, nos. 1-3, pp. 45-84, 2008.
[25] S. Akshay, B. Bollig, P. Gastin, M. Mukund, and K. Narayan Kumar, "Distributed Timed Automata with Independently Evolving Clocks," Proc. 19th Int'l Conf. Concurrency Theory, pp. 82-97, 2008.
[26] G. Rodriguez-Navas, J. Proenza, H. Hansson, and P. Pettersson, "Using Timed Automata for Modeling the Clocks of Distributed Embedded Systems," Behavioral Modeling for Embedded Systems and Technologies: Applications for Design and Implementation, IGI Global, 2010.
[27] T.A. Henzinger, P.W. Kopke, A. Puri, and P. Varaiya, "What's Decidable about Hybrid Automata?" J. Computer and System Sciences, vol. 57, no. 1, pp. 94-124, 1998.