Title :
Cyber-Physical System Components Composition Analysis and Formal Verification Based on Service-Oriented Architecture
Author :
Peng Wang ; Yang Xiang ; Shao Hua Zhang
Author_Institution :
Coll. of Electron. & Inf. Eng., Tongji Univ., Shanghai, China
Abstract :
How to design a distributed and open-ended Cyber-Physical system (CPS) architecture is an important issue for constructing different CPS business applications. In this paper, a service-oriented architecture is proposed, in which software and hardware components are represented in the form of interoperable CPS services. CPS services are combined to realize complicated business requirements. Further, a formal method for verifying validity of CPS service composition model is put forward based on Time-Space π-calculus, which is presented through introducing time operator and space operator into π-calculus. Finally, a case study is performed to show that how to apply the model and method to CPS components composition. The experiment result shows that they are reasonable and feasible.
Keywords :
formal verification; object-oriented programming; open systems; pi calculus; service-oriented architecture; CPS architecture; CPS business applications; CPS service composition model; complicated business requirements; cyber-physical system components composition analysis; distributed cyber-physical system architecture; formal method; formal verification; hardware components; interoperable CPS services; open-ended cyber-physical system architecture; service-oriented architecture; software components; space operator; time-space π-calculus; verifying validity; Accidents; Business; Computer architecture; Monitoring; Process control; Service oriented architecture; Vehicles; Cyber-Physical system; Service Composition; Service-Oriented Architecture; Time-Space p-calculus;
Conference_Titel :
e-Business Engineering (ICEBE), 2012 IEEE Ninth International Conference on
Conference_Location :
Hangzhou
Print_ISBN :
978-1-4673-2601-8
DOI :
10.1109/ICEBE.2012.60