Thanh Nguyen Tien
ABSTRACT
To design and analyze Cyber-Physical Systems (CPSs), engineers should consider computation and physical processes at the same time. Engineers require a design description which is easy to understand. SysML provides diagrammatic notations which are independent of specific disciplines. To express numerical constraints of SysML diagrams, we extend OCL with real arithmetic. Both SysML and extended-OCL require an executable design language to check inconsistencies of constraints. To achieve the above idea, we bridge a gap between SysML and VDM-RT. We propose a framework to embed SysML/extended-OCL into VDM-RT, where we prepare some libraries for extended-OCL. It is unnecessary for engineers to know VDM-RT. Using a unified CPS design description, our approach automatically debugs inconsistencies in whole CPS design. This paper illustrates the proposed method with a car race system.
- Object Management Group 2012. OMG System Modeling Language Specification. Retrieved March 6, 2012 from http://www.omg.org/spec/SysML/1.3/.Google Scholar
- Object Management Group 2012. OMG Object Constraint Language. Retrieved March 6, 2012 from http://www.omg.org/spec/OCL/2.3.1Google Scholar
- Lee, E. A. 2008. Cyber-Physical Systems: Design challenges. Object Oriented Real-Time Distributed Computing (ISORC), 11th IEEE International Symposium, 7 (May), 363--369. Google ScholarDigital Library
- Richters, M. 2002. A precise approach to validating UML models and OCL constraints, Ph.D. Dissertation. Universitat Bremen, Fachbereich Mathematik und Informatik, Logos Verlag, Berlin, BISS Monographs, No. 14.Google ScholarDigital Library
- Bradley, A. B., Manna, Z. 2007. The Calculus of Computation-Decision Procedures with Application to Verification. Springer. Google ScholarDigital Library
- Nakajima, S., Furukawa, S., Ueda, Y. 2012. Co-analysis of SysML and Simulink Models for Cyber-Physical Systems Design. Proc. RTCSA2012, 22 (August), 473--478. Google ScholarDigital Library
- Fitzgerald, J. et al 2010. Collaborative Modelling and Co-simulation in the Development of Dependable Embedded Systems. Integrated Formal Methods, 11 (October), 12--26. Google ScholarDigital Library
- Brummayer, R., Biere, A. 2009. Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. TACAS2009, 29 (March), 174--177. Google ScholarDigital Library
- Kato, H., Ueda, Y., Nakajima, S. 2010. A Study on Validation of SysML Model Constraints (in Japanese). Proc. ESS2010.Google Scholar
- Gogolla, M., Büttner, F., Richters, M. 2007. USE: A UML-based Specification Environment for Validating UML and OCL. Science of Computer Programming 69.1, 19 (December), 27--34. Google ScholarDigital Library
- Jackson, D., Schechter, I., Shlyakhter, I. 2000. ALCOA: The Alloy Constraint Analyzer. Proceedings of the 2000 International Conference, IEEE, 11 (June), 730--733. Google ScholarDigital Library
- Wille, R., Soeken, M., Drechsler, R. 2012. Debugging of inconsistent UML/OCL models. Proceedings of the Conference on Design, Automation and Test in Europe, 16 (March), 1078--1083. Google ScholarDigital Library
- IBM Rational Rhapsody, http://www-142.ibm.com/software/products/us/en/ratirhapfami/.Google Scholar
- Hussmann, H., Demuth, B., Finger, F. 2000. Modular architecture for a toolset supporting OCL. The Unified Modeling Language. Springer Berlin Heidelberg, 6 (October), 278--293. Google ScholarDigital Library
- Soeken, M. et al 2010. Verifying UML/OCL models using Boolean satisfiability. Proceedings of the Conference on Design, Automation and Test in Europe, 11 (March), 1341--1344. Google ScholarDigital Library
- Larsen, P. G., Fitzgerald, J., Wolff, S. 2009. Methods for the Development of Distributed Real-Time Systems using VDM. International Journal of Software and Informatics 3(2--3), 9 (August), 305--341.Google Scholar
- Clarke, E. M., Zuliani, P. 2011. Statistical Model Checking for Cyber-Physical Systems. Automated Technology for Verification and Analysis, 12 (October), 1--12. Google ScholarDigital Library
- Ge, N., Nakajima, S., Pantel, M. 2013. Efficient online analysis of accidental fault localization for dynamic systems using hidden Markov model. Proceedings of the Symposium on Theory of Modeling and Simulation-DEVS Integrative M and S Symposium, 8 (April), 16--24. Google ScholarDigital Library
- Vanderperren, Y. et al 2008. UML for electronic systems design: a comprehensive overview. Design automation for embedded systems 12.4, 1 (December), 261--292.Google Scholar
- Li, C. M., Manya, F. 2009. MaxSAT, Hard and Soft Constraints. Handbook of Satisfiability, 613--631.Google Scholar
- Dutertre, B., de Moura, I. 2006 The YICES SMT Solver. http://yices.csl.sri.com/.Google Scholar
Index Terms
- Modeling and debugging numerical constraints of cyber-physical systems design
Recommendations
INTEGRATED PRODUCT DEVELOPMENT APPROACH FOR CYBER-PHYSICAL SYSTEMS UTILIZING STANDARDIZED MODELING LANGUAGES AND METHODOLOGIES
Systems development has often resulted as a hit-or-miss proposition before the advent of standardized analysis and design languages providing blueprints understood by both software and systems engineers. This paved the way for modeling cyber-physical ...
Geometrical Meta-Metamodel for Cyber-Physical Modelling
CW '13: Proceedings of the 2013 International Conference on CyberworldsExisting metamodels are not able to effectively capture the knowledge of multidimensional cyber-physical domains. In order to contribute to this area the approach for development of metamodels for modelling the multidimensional cyber-physical systems is ...
Convergence Approach to Model Physical World and Cyber World of Aviation Cyber Physical System
DASC '14: Proceedings of the 2014 IEEE 12th International Conference on Dependable, Autonomic and Secure ComputingAviation Cyber-Physical Systems are the integration of cyber systems and physical systems. Recent concentration to Aviation Cyber Physical Systems (ACPS) is driven by the demand for deeper Convergence of design disciplines that integrate physical and ...
Comments