JTCSP Modeling Language Research And Tool Design And Implementation

For safety-critical systems such as rail transit and aerospace,the correctness,safety,real-time and reliability of the system are all crucial,and such computer systems often rely on quantitative timing.With the continuous development of system functions and performance,the system architecture tends to be more modular,and its layered structure is becoming more and more complex.The work related to modeling and verification of real-time systems is also facing great challenges.The choice of modeling language for realtime systems is also a non-negligible factor affecting the analysis and model checking of the entire system.The modeling language needs to cover the requirements of all aspects,and the semantic model needs to intuitively and accurately reflect the effectiveness of the system’s behavior and related attributes.The mainstream real-time system modeling languages include Timed CCS,Timed CSP,and Timed Automata,among which Timed Automata and Timed CSP are often used for modeling and verification of real-time systems.A timed automaton is essentially a finite state machine with a clock variable.It is excellent in designing models with explicit clock variables.It models time as a continuous real number variable,which can represent various timing behaviors in the system,and Supports formal verification of the timing properties of the system.Models based on timed automata usually adopt a simple structure,but for layered complex real-time systems,they are usually expressed in terms of delay,timeout,waiting time,interruption,etc.Timed automata lack high-level combination patterns for layered design,Therefore,when using time automata for modeling,it is necessary to manually convert these time terms into a set of clock variables with time constraints.This conversion process is cumbersome and error-prone.Poor readability,difficult to modify and maintain.So there are certain defects in using timed automata to model hierarchical complex real-time systems.For Timed CSP,it is based on CSP and extends clock constraints to describe the time behavior in concurrent systems.Although it provides a process-based description,it can better describe the hierarchical structure,but for complex real-time systems,the model It may become too complicated,making the model unreadable,difficult to maintain and modify,and Timed CSP’s ability to describe continuous time systems is relatively weak.Therefore,for application scenarios that need to describe hierarchical real-time systems,factors such as model readability,accuracy,expressiveness,and modeling complexity need to be considered comprehensively.This paper proposes a modeling language called jTCSP,which is an extension based on Timed CSP,inheriting and extending concepts such as process and clock constraints.At the same time,it combines the Java high-level programming language to simplify the layered design and support complex and flexible data structures.It aims to make up for the disadvantages of Timed CSP in modeling layered real-time systems,and can effectively model layered complex real-time systems.In addition,the jTCSP modeling language is designed to be executable,and a model checking tool for the jTCSP modeling language is implemented,which can automatically and efficiently perform model checking.