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

## 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## Preview

Unable to display preview. Download preview PDF.

## References

- 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.Ben-Ari, M.:
*Principles of concurrent programming*, Prentice-Hall International, 1982.Google Scholar - 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.Chaochen, Z.: Duration calculi: an overview,
*International Institute for Software Technology, The United Nations University, UNI/IIST Report*,**10**(1993).Google Scholar - 5.E. W. Dijkstra: Co-operating sequential process,
*Programming Languages*(1968), pp, 43–112.Google Scholar - 6.Hoare, C. A. R.:
*Communicating Sequential Processes*, Prentice-Hall International (1985).Google Scholar - 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.Igarashi, S.: Verification of programs,
*Journal of Information Processing Society of Japan*,**19**(1978), pp. 1003–1010 (in Japanese).Google Scholar - 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.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.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.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.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.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.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.Kröger, F.:
*Temporal logic of programs*, Springer-Verlag (1987).Google Scholar - 17.Lamport, L.: What good is temporal logic?, in R. E. A. Mason (ed.),
*Inf. Proc. 83*(1983), pp. 657–668.Google Scholar - 18.Manna, Z. and Pnueli, A.: Completing the temporal picture,
*Theor. Comp. Sci*,**83**(1991), pp. 97–130.CrossRefGoogle Scholar - 19.Manna, Z. and Pnueli, A.:
*The temporal logic for reactive and concurrent systems specification*, Springer-Verlag (1992).Google Scholar - 20.Majumdar, R. and Shyamasundar, R. K.: design of controllers for linear hybrid systems,
**1179**(1996), pp. 309–320.Google Scholar - 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.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.Moszkowski, B. C.:
*Executing temporal logic programs*, Cambridge Univ. Press (1986).Google Scholar - 24.Takeuti, G.:
*Two applications of logic to mathematics*, Princeton University Press (1978).Google Scholar - 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.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.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.Xuandong, L. and Hung, D. V.: Checking linear duration invariants by linear programming,
**1179**(1996), pp. 321–330.Google Scholar