Advertisement

Real-Time Systems Development with Duration Calculi: An Overview

  • Dang Van Hung
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2757)

Abstract

In this paper we present the main achievements of UNU/IIST during the project “Design Techniques for Real-time Systems” carried out since 1993 by its staff and fellows. Duration Calculus was originally introduced in 1991 as a powerful logic for specifying the safety of real-time systems. During the project, it has evolved to a set of calculi that can capture many important aspects in real-time systems development including techniques for specification, design, discretisation and verification. These techniques are discussed informally in the paper.

Keywords

IEEE Computer Society Operational Semantic Proof System Programmable Logic Controller Time Automaton 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Asarin, E., Caspi, P., Maler, O.: A Kleene Theorem for Timed Automata. In: Winskel, G. (ed.) International Symposium on Logics in Computer Science LICS 1997, pp. 160–171. IEEE computer Society Press, Los Alamitos (1997)Google Scholar
  2. 2.
    Barua, R., Chaochen, Z.: Neighbourhood Logics: NL and NL2. Presented at ComBaS Group, Technical University of Denmark, September 4-7 (1997)Google Scholar
  3. 3.
    Chan, P., Van Hung, D.: Duration Calculus Specification of Scheduling for Tasks with Shared Resources. In: Kanchanasut, K., Levy, J.-J. (eds.) ACSC 1995. LNCS, vol. 1023, pp. 365–380. Springer, Heidelberg (1995)Google Scholar
  4. 4.
    Chaochen, Z., Guelev, D.P., Naijun, Z.: A Higher-Order Duration Calculus. Published in: the proceedings of the Symposium in Celebration of the Work of C.A.R. Hoare, Oxford, September 13-15 (1999)Google Scholar
  5. 5.
    Chaochen, Z., Hansen, M.R.: An Adequate First Order Interval Logic. In: Langmaack, H., et al. (eds.) International Symposium, Compositionality - The Significant Difference, Springer, Heidelberg (1998)Google Scholar
  6. 6.
    Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Chaochen, Z., Van Hung, D., Xiaoshan, L.: A Duration Calculus with Infinite Intervals. In: Reichel, H. (ed.) FCT 1995. LNCS, vol. 965, pp. 16–41. Springer, Heidelberg (1995)Google Scholar
  8. 8.
    Chaochen, Z., Jingzhong, Z., Lu, Y., Xiaoshan, L.: Linear Duration Invariants. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863. Springer, Heidelberg (1994)Google Scholar
  9. 9.
    Chaochen, Z., Hansen Michael, R., Sestoft, P.: Decidability and Undecidability Results in Duration Calculus. In: Enjalbert, P., Wagner, K.W., Finkel, A. (eds.) STACS 1993. LNCS, vol. 665. Springer, Heidelberg (1993)Google Scholar
  10. 10.
    Chaochen, Z., Xiaoshan, L.: A Mean Value Duration Calculus. In: A Classical Mind, Festschrift for C.A.R. Hoare, pp. 432–451. Prentice-Hall International, Englewood Cliffs (1994)Google Scholar
  11. 11.
    Dierks, H., Fehnker, A., Mader, A., Vaandrager, F.: Operational and Logical Semantics for Polling Real-Time Systems. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 29–40. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  12. 12.
    Dong, L.X., Van Hung, D.: Checking Linear Duration Invariants by Linear Programming. In: Jaffar, J., Yap, R.H.C. (eds.) ASIAN 1996. LNCS, vol. 1179, pp. 321–332. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  13. 13.
    Dong, L.X., Van Hung, D., Tao, Z.: Checking Hybrid Automata for Linear Duration Invariants. In: Shyamasundar, R.K. (ed.) ASIAN 1997. LNCS, vol. 1345, pp. 166–180. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  14. 14.
    George, C., Yong, X.: An Operational Semantics for Timed RAISE. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1008–1027. Springer, Heidelberg (1999)Google Scholar
  15. 15.
    Guelev, D.P.: A Complete Fragment of Higher-Order Duration μ-Calculus. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol. 1974, pp. 264–276. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  16. 16.
    Guelev, D.P.: Probabilistic Neighbourhood Logic. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 264–275. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  17. 17.
    Guelev, D.P., Van Hung, D.: Prefix and Projection onto State in Duration Calculus. Electronic Notes in Theoretical Computer Science 65(6) (2002)Google Scholar
  18. 18.
    Hansen, M.R.: Model-checking Discrete Duration Culculus. Formal Aspects ofComputing 6(6A), 826–845 (1994)zbMATHCrossRefGoogle Scholar
  19. 19.
    Hansen, M.R., Chaochen, Z.: Chopping a point. In: Hansen, M.R., Chaochen, Z. (eds.) BCS-FACS 7th refinement workshop, Electronics Workshops in Computing. Springer, Heidelberg (1996)Google Scholar
  20. 20.
    Hansen, M.R., Chaochen, Z.: Duration calculus: Logical foundations. Formal Aspects of Computing 9, 283–330 (1997)zbMATHCrossRefGoogle Scholar
  21. 21.
    Huibiao, Z., Jifeng, H.: A DC-based Semantics for Verilog. In: Feng, Y., Notkin, D., Gaudel, M.-C. (eds.) Published in the proceedings of the ICS2000, Beijing, August 21-24, pp. 421–432 (2000)Google Scholar
  22. 22.
    Van Hung, D.: Modelling and Verification of Biphase Mark Protocols in Duration Calculus Using PVS/DC . In: The proceedings of CSD 1998, Aizu-wakamatsu, Fukushima, Japan, March 23-26, pp. 88–98. IEEE Computer Society Press, Los Alamitos (1998)Google Scholar
  23. 23.
    Van Hung, D.: Projections: A Technique for Verifying Real-Time Programs in Duration Calculus. Technical Report 178, UNU/IIST, Macau (November 1999)Google Scholar
  24. 24.
    Van Hung, D., Chaochen, Z.: Probabilistic Duration calculus for Continuous Time. Formal Aspects of Computing 11, 21–44 (1999)zbMATHCrossRefGoogle Scholar
  25. 25.
    Van Hung, D., Guelev, D.P.: Completeness and Decidability of a Fragment of Duration Calculus with Iteration. In: Thiagarajan, P.S., Yap, R.H.C. (eds.) ASIAN 1999. LNCS, vol. 1742, pp. 139–150. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  26. 26.
    Van Hung, D., Kwang Il, K.: Verification via Digitized Model of Real-Time Systems. In: Published in the proceedings of Asia-Pacific Software Engineering Conference 1996 (APSEC 1996), pp. 4–15. IEEE Computer Society Press, Los Alamitos (1996)CrossRefGoogle Scholar
  27. 27.
    Van Hung, D., Ji, W.: On The Design of Hybrid Control Systems Using Automata Model. In: Chandru, V., Vinay, V. (eds.) FSTTCS 1996. LNCS, vol. 1180, pp. 156–167. Springer, Heidelberg (1996)Google Scholar
  28. 28.
    Jianhua, Z., Van Hung, D.: Checking Timed Automata for Some Discreti-sable Duration Properties. Journal of Computer Science and Technology 15(5), 423–429 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  29. 29.
    Jianzhong, W., Qiwen, X., Huadong, M.: Modelling and Verification of Network Player System with DCValid. In: The proceedings of the First Asia-Pacific Conference on Quality Software, Hong Kong, October 2000, pp. 44–49. IEEE Computer Society Press, Los Alamitos (2000)CrossRefGoogle Scholar
  30. 30.
    Jifeng, H.: A behavioural Model for Co-design. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1420–1439. Springer, Heidelberg (1999)Google Scholar
  31. 31.
    Jifeng, H.: An Integrated Approach to Hardware/Software Co-design. In: Feng, Y., Notkin, D., Gaudel, M.-C. (eds.) Published in the proceedings of the ICS2000, Beijing, August 21-24 (2000)Google Scholar
  32. 32.
    Jifeng, H., Qiwen, X.: Advanced Features of DC and Their Applications. In: The proceedings of the Symposium in Celebration of the Work of C.A.R. Hoare, Oxford, September 13-15 (1999)Google Scholar
  33. 33.
    Jifeng, H., Qiwen, X.: An Operational Semantics of a Simulator Algorithm. In: The proceedings of the PDPTA 2000, Las Vegas, Nevada, USA, June 26-29 (2000)Google Scholar
  34. 34.
    Jifeng, H., Verbovskiy, V.: Integrating CSP and DC. In: Published in the proceedings of the 8th IEEE International Conference on Engineering of Complex Computer Systems, Maryland, USA, December 2-4 (2002)Google Scholar
  35. 35.
    Li, L., Jifeng, H.: Towards a Denotational Semantics of Timed RSL using Duration Calculus. Chinese Journal of Advanced Software Research (2000)Google Scholar
  36. 36.
    Martin, F.: Synthesizing Controllers of Duration Calculus. In: Jonsson, B., Parrow, J. (eds.) FTRTFT 1996. LNCS, vol. 1135, pp. 168–187. Springer, Heidelberg (1996)Google Scholar
  37. 37.
    Moore, J.S.: A Formal Model of Asynchronous Communication and Its Use in Mechanically Verifying a Biphase Mark Protocol. FAC 6, 60–91 (1994)zbMATHCrossRefGoogle Scholar
  38. 38.
    Naijun, Z.: Completeness of Higher-Order Duration Calculus. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, p. 442. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  39. 39.
    Van Nhon, D., Van Hung, D.: A Systematic Design of Real-time Systems Using Duration Calculus. In: Published in the proceedings of the conference SCI 2001, Orlando, USA, July 22-25, pp. 241–246. IEEE Computer Society Press, Los Alamitos (2001)Google Scholar
  40. 40.
    Pandya, P.K., Van Hung, D.: Duration Calculus with Weakly Mono- tonic Time. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 55–64. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  41. 41.
    Pandya, P.K.: Y Ramakrishna. A Recursive Duration Calculus. Technical Report CS-95/3, TIFR, Mumbai (1995)Google Scholar
  42. 42.
    Pandya, P.K., Hanpin, W., Qiwen, X.: Towards a Theory of Sequential Hybrid Programs. In: Gries, D., de Roever, W. (eds.) The proceedings of PROCOMET 1998, Shelter Island, New York, USA, June 8-12, pp. 366–384. Chapman & Hall, Boca Raton (1998)Google Scholar
  43. 43.
    Pavlova, E., Van Hung, D.: A Formal Specification of the Concurrency Control in Real-Time Databases. In: the proceedings of APSEC 1999, Takamatsu, Japan, December 7-10, pp. 94–101. IEEE Computer Society Press, Los Alamitos (1999)Google Scholar
  44. 44.
    Qiwen, X.: Semantics and Verification of the Extended Phase Transition Systems in the Duration Calculus. In: Maler, O. (ed.) HART 1997. LNCS, vol. 1201, pp. 301–315. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  45. 45.
    Qiwen, X., Naijun, Z.: Formalising Scheduling Theories in Duration Calculus. Technical Report 243, UNU/IIST, P.O. Box 3058, Macau (October 2001)Google Scholar
  46. 46.
    Satpathy, M., Van Hung, D., Pandya, P.K.: Some Results on The Decidability of Duration Calculus under Synchronous Interpretation. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 186–197. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  47. 47.
    Siewe, F., Van Hung, D.: From Continuous Specification to Discrete Design. In: Feng, Y., Notkin, D., Gaudel, M.-C. (eds.) Published in the proceedings of the ICS2000, Beijing, August 21-24, pp. 407–414 (2000)Google Scholar
  48. 48.
    Siewe, F., Van Hung, D.: Deriving Real-Time Programs from Duration Calculus Specifications. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 92–97. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  49. 49.
    Tapken, J., Dierks, H.: MOBY/PLC - Graphical Development of PLC-Automata. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 311–314. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  50. 50.
    Thae, H.K., Van Hung, D.: Formal Design of Hybrid Control Systems: Duration Calculus Approach. In: The proceedings of COMPSAC 2001, Chicago, USA, October 8-12, pp. 423–428. IEEE Computer Society Press, Los Alamitos (2001)Google Scholar
  51. 51.
    Venema, Y.: A modal logic for chopping intervals. Journal of Logic Computation 1(4), 453–476 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  52. 52.
    Weidong, H., Chaochen, Z.: A Case Study of Optimization. The Computer Journal 38(9), 734–746 (1995)CrossRefGoogle Scholar
  53. 53.
    Yong, L., Van Hung, D.: Checking Temporal Duration Properties of Timed Automata. Journal of Computer Science and Technology 17(6), 689–698 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  54. 54.
    Yuhua, Z., Chaochen, Z.: A Formal Proof of a Deadline Driven Scheduler. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 756–775. Springer, Heidelberg (1994)Google Scholar
  55. 55.
    Zhiming, L., Sørensen, E.V., Anders, R.P., Chaochen, Z.: Towards a calculus of systems dependability. Journal of High Integrity Systems 1(1), 49–65 (1994)Google Scholar
  56. 56.
    Zongji, C., Ji, W., Chaochen, Z.: An Abstraction of Hybrid Control Systems. Research Report 26, UNU/IIST, Macau (June 1994)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Dang Van Hung
    • 1
  1. 1.The United Nations University International Institute for Software TechnologyMacau

Personalised recommendations