Advertisement

Representation of discretely controlled continuous systems in software-oriented formal analysis

  • Tetsuya Mizutani
  • Shigeru Igarashi
  • Kohji Tomita
  • Masayuki Shio
Session 3
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1345)

Abstract

We have already introduced and demonstrated a new formalism SOFA to analyze and verify programs that control discretely certain continuously physical or other external systems, based on the analytical semantics. Using this formalism, program specifications and its behavior can be not only expressed easily but also directly translated into the conventional mathematics including differential equations. We obtain the actual rational time value when the next action from an observation time will rise, so that verification can be easier and more precise. Other verification systems, for example the verification diagram for reactive system, do not treat realtime system explicitly, so that they do not formulated various physical phenomena straightforward. Some examples, the leaking gas burner model and the autonomous vehicle control system, etc., will be represented, analyzed and verified formally.

Keywords

Temporal Logic Program Variable Hybrid Automaton Time Symbol Duration Calculus 
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.
    Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T. A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J. and Yovine, S.: The algorithmic analysis of hybrid systems, Theoretical Computer Science, 138 (1995), pp. 3–34.CrossRefGoogle Scholar
  2. 2.
    Ben-Ari, M.: Principles of concurrent programming, Prentice-Hall International, 1982.Google Scholar
  3. 3.
    Browne, I. A., Manna, Z. and Sipma, H. B.: Hierarchical verification using verification diagrams, Concurrency and Parallelism, Programming, Networking, and Security, Lecture notes in computer science, 1179 (1996), pp. 276–286.Google Scholar
  4. 4.
    Chaochen, Z.: Duration calculi: an overview, International Institute for Software Technology, The United Nations University, UNI/IIST Report, 10 (1993).Google Scholar
  5. 5.
    E. W. Dijkstra: Co-operating sequential process, Programming Languages (1968), pp, 43–112.Google Scholar
  6. 6.
    Hoare, C. A. R.: Communicating Sequential Processes, Prentice-Hall International (1985).Google Scholar
  7. 7.
    Igarashi, S.: An axiomatic approach to the equivalence problems of algorithms with applications, Rep. Comp. Centre Univ. Tokyo, 1 (1968), pp. 1–101.Google Scholar
  8. 8.
    Igarashi, S.: Verification of programs, Journal of Information Processing Society of Japan, 19 (1978), pp. 1003–1010 (in Japanese).Google Scholar
  9. 9.
    Igarashi, S.: The χ-conversion and an analytic semantics, in Mason, R. E. A. (ed.), Inf. Proc. 83 (1983), pp. 769–774.Google Scholar
  10. 10.
    Igarashi, S., Mizutani, T. and Tsuji, T.: An analytical semantics of parallel program processes represented by χ-conversion., TENSOR, N. S., 45 (1987), pp. 222–228.Google Scholar
  11. 11.
    Igarashi, S., Mizutani, T. and Tsuji, T.: Specifications of parallel program processes in analytical semantics., TENSOR, N. S., 45 (1987), pp. 240–244.Google Scholar
  12. 12.
    Igarashi, S., Tsuji, T., Mizutani, T. and Haraguchi, T.: Experiments on Computerized Piano Accompaniment, Proceedings of the 1993 International Computer Music Conference (1993), pp. 415–417.Google Scholar
  13. 13.
    Igarashi, S., Mizutani, T., Tsuji, T. and Hosono, C.: On locomorphism in analytical equivalence theory, in Jones, N. D., Hagiya, M. and Sato, M. eds., Logic, Language and Computation: Festschrift in Honor of Satoru Takasu, Lecture notes in computer science, 792 (1994), pp. 173–187.Google Scholar
  14. 14.
    Igarashi, S., Mizutani, T., Shirogane, T. and Shio, M.: Formal analysis for continuous systems controlled by programs, Concurrency and Parallelism, Programming, Networking, and Security, Lecture notes in computer science, 1179 (1996), pp. 347–348.Google Scholar
  15. 15.
    Igarashi, S., Shio, M., Shirogane, T. and Mizutani, T.: Formal verification and evaluation of execution time in the envelope theory, Concurrency and Parallelism, Programming, Networking, and Security, Lecture notes in computer science, 1179 (1996), pp. 299–308.Google Scholar
  16. 16.
    Kröger, F.: Temporal logic of programs, Springer-Verlag (1987).Google Scholar
  17. 17.
    Lamport, L.: What good is temporal logic?, in R. E. A. Mason (ed.), Inf. Proc. 83 (1983), pp. 657–668.Google Scholar
  18. 18.
    Manna, Z. and Pnueli, A.: Completing the temporal picture, Theor. Comp. Sci, 83 (1991), pp. 97–130.CrossRefGoogle Scholar
  19. 19.
    Manna, Z. and Pnueli, A.: The temporal logic for reactive and concurrent systems specification, Springer-Verlag (1992).Google Scholar
  20. 20.
    Majumdar, R. and Shyamasundar, R. K.: design of controllers for linear hybrid systems, Concurrency and Parallelism, Programming, Networking, and Security, Lecture notes in computer science, 1179 (1996), pp. 309–320.Google Scholar
  21. 21.
    Mizutani, T., Hosono, C. and Igarashi, S.: Verification of programs using χ-definable acts, Computer Software, 2 (1985), pp. 529–538 (in Japanese).Google Scholar
  22. 22.
    Mizutani, T., Igarashi, S. and Tsuji, T.: An analytical equivalence theory of computer programs, Proceedings of International Symposium on Structures in Mathematical Theories (1990), pp. 199–204.Google Scholar
  23. 23.
    Moszkowski, B. C.: Executing temporal logic programs, Cambridge Univ. Press (1986).Google Scholar
  24. 24.
    Takeuti, G.: Two applications of logic to mathematics, Princeton University Press (1978).Google Scholar
  25. 25.
    Tomita, K., Tsuji, T. and Igarashi, S.: Analysis of a software/hardware system by tense arithmetic, in Jones, N. D., Hagiya, M. and Sato, M. eds., Logic, Language and Computation: Festschrift in Honor of Satoru Takasu, Lecture notes in computer science, 792 (1994), pp. 188–205.Google Scholar
  26. 26.
    Tomita, K., Igarashi, S., Hosono, C., Mizutani, T. and Tsugawa, S.: Representations of autonomous realtime systems, The 4th International Conference of Tensor Society on Differential Geometry and its Applications, Tsukuba, 1996. (TENSOR, N.S., submitted to.)Google Scholar
  27. 27.
    Tsugawa, S. and Murata, S.: Steering control algorithm for autonomous vehicle, Proc. Japan-U.S.A. Symposium on Flexible Automation (1990), 143–146.Google Scholar
  28. 28.
    Xuandong, L. and Hung, D. V.: Checking linear duration invariants by linear programming, Concurrency and Parallelism, Programming, Networking, and Security, Lecture notes in computer science, 1179 (1996), pp. 321–330.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Tetsuya Mizutani
    • 1
  • Shigeru Igarashi
    • 1
  • Kohji Tomita
    • 2
  • Masayuki Shio
    • 1
  1. 1.Institute of Information ScienceUniversity of TsukubaJapan
  2. 2.Mechanical Engineering Laboratory, AIST, MITITsukubaJapan

Personalised recommendations