AUTHORS: Yeongbok Choe, Sunghyeon Lee, Moonkun Lee
Download as PDF
ABSTRACT: There are strong needs for both mobile and temporal properties in process algebras designed to specify and analyze distributed mobile real-time systems (DMRS). However there are some limitations in those algebras to specify both movements and temporalness at the same time, such as, Timed pi-Calculus and d-Calculus, as follows: 1) Timed pi-Calculus cannot specify both the execution time of action and movements directly, and 2) d-Calculus can specify only a simple pattern of temporal conditions, that is, the lower and upper bounds of the execution time. In order to solve these limitations, this paper proposes dT-Calculus with expressive power of movements of processes with a number of temporal conditions. dT-Calculus extended the basic temporal properties of synchronous process movements of d-Calculus into more specific temporal properties in order to specify and analyze the temporal property of DMRS more effectively: ready time, execution time, waiting time, deadline, etc. In order to simulate the proposed process movement with temporal properties, the SAVE tool has been developed on the ADOxx Meta-Modeling Platform and demonstrates efficiency and effectiveness of the proposed approach with an EMS example.
KEYWORDS: dT-calculus, d-calculus, Process Algebra, Mobility, Time, SAVE
REFERENCES:
[1] Haxthausen AE, Peleska Jan. Formal development and verification of a distributed railway control system. Software Engineering IEEE Transactions on Vol. 26, No. 8. August. 2000. pp. 687-701.
[2] N.Saeedloei and G.Gupta, Timed π-Calculus, Trustworthy Global Computing. TGC 2013. Lecture Notes in Computer Science, vol 8358. Springer, Cham, 2014.
[3] Y. Choe and M. Lee, δ-Calculus: Process Algebra to Model Secure Movements of Distributed Mobile Processes in Real-Time Business Application, 23rd European Conference on Information Systems, 2015.
[4] R. Milner, J. Parrow and D. Walker, 'A calculus of mobile processes(i-ii),' Information and Computation, pp. 1-77, 1992.
[5] Y. Choe, W. Choi, G. Jeon and M. Lee, A Tool for Visual Specification and Verification for Secure Process Movements, eChallenges e-2015, November 2015.
[6] H. Fill and D. Karagiannis, On the Conceptualisation of Modeling Methods Using the ADOxx Meta Modeling Platform, Enterprise Modeling and Information Systems Architectures 8(1), pp.4-25, 2013.
[7] S. Lee, Y. Choe and M. Lee, A Dual Method to Model IoT Systems, International Journal of Mathematical Models and Methods in Applied Sciences, Volume 10, pp. 210-219, 2016. Acknowledgment This work was supported by Basic Science Research Programs through the National Research Foundation of Korea(NRF) funded by the Ministry of Education(2010- 0023787), and Space Core Technology Development Program through the NRF(National Research Foundation of Korea) funded by the Ministry of Science, ICT and Future Planning(NRF-2014M1A3A3A02034792), and Basic Science Research Program through the National Research Foundation of Korea(NRF) funded by the Ministry of Education(NRF-2015R1D1A3A01019282).
