zbMATH — the first resource for mathematics

Synergistic verification and validation of systems and software engineering models. (English) Zbl 1191.68180
Summary: We present a unified approach for the verification and validation of software and systems engineering design models expressed in UML 2.0 and SysML 1.0. The approach is based on three well-established techniques, namely formal analysis, programme analysis and software engineering (SwE) techniques. More precisely, our contribution consists of the synergistic combination of model checking, static analysis and SwE metrics that enables the automatic and efficient assessment of design models from static and dynamic perspectives. Additionally, we present the design and implementation of an automated computer-aided assessing framework integrating the proposed approach. Moreover, we discuss the related technical details and the underlying synergism. Finally, we illustrate the proposed approach by assessing a design case study that is composed of state machine and sequence diagrams.
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Full Text: DOI
[1] Abreu F., Object-oriented software engineering: measuring and controlling the development process (1994)
[2] Abreu, F. and Melo, W. 1996.Evaluating the impact of object-oriented design on software quality, 90–99. Washington, DC: IEEE Computer Society.
[3] Alawneh, L. 2006.A unified approach for verification and validation of systems and software engineering models, 409–418. Washington, DC: IEEE Computer Society.
[4] DOI: 10.1017/CBO9780511584077 · doi:10.1017/CBO9780511584077
[5] Averant, I., 2001. Static functional verification with solidify, a new low-risk methodology for faster debug of ASICs and programmable parts, Technical report, Averant, Inc
[6] Ben-David, S. 2000.Scalable distributed on-the-fly symbolic model checking, 390–404. Berlin/Heidelberg: Springer.
[7] Boehm B.W., IEEE computer 34 pp 135– (2001)
[8] Bozga, M. 1999.IF: an intermediate representation and validation environment for timed asynchronous systems, 307–327. Berlin/Heidelberg: Springer.
[9] Briand, L.C., Devanbu, P.T. and Melo, W.L. 1997.An investigation into coupling measures for C++, 412–421. New York, NY: ACM.
[10] Burch, J. 1990.Symbolic model checking: 1020 states and beyond, 1–33. Washington, DC: IEEE Computer Society Press.
[11] Cengarle, M.V. and Knapp, A. 2004.UML 2.0 interactions: semantics and refinement, 85–99. München: Technische Universität München.
[12] DOI: 10.1109/32.295895 · Zbl 05113989 · doi:10.1109/32.295895
[13] Cimatti, A. 1999.NUSMV: a new symbolic model verifier, 495–499. London: Springer. · Zbl 1046.68587
[14] Dasgupta, P., Chakrabarti, A. and Chakrabarti, P.P. 2002.Open computation tree logic for formal verification of modules, 735Washington, DC: IEEE Computer Society.
[15] Fecher, H., Kyas, M. and Schönborn, J., 2005. Semantic issues in UML 2.0 state machines, Technical report 0507, Christian-Albrechts-Universität zu Kiel
[16] Genero M., L’Objet 6 pp 489– (2000)
[17] Gronback, R., 2004. Model validation: applying audits and metrics to UML models, Borland Developer Conference, Borland Software Corporation
[18] Grosu, R. and Smolka, S.A. 2005.Safety-liveness semantics for UML 2.0 sequence diagrams, 6–14. Washington, DC: IEEE Computer Society. June
[19] DOI: 10.1109/32.588521 · Zbl 05113845 · doi:10.1109/32.588521
[20] Hsin-Hung, L., 2003. A research of model checking UML statechart diagrams. Master’s thesis. Japan Advanced Institute of Science and Technology
[21] IEEE, 1990. IEEE Std 610.12-1990, IEEE standard glossary of software engineering terminology, Technical report, IEEE
[22] Jarraya, Y. 2007.Automatic verification and performance analysis of time-constrained SysML activity diagrams, 515–522. Los Alamitos, CA: IEEE Computer Society.
[23] Knapp, A., Merz, S. and Rauh, C. 2002.Model checking – timed UML state machines and collaborations, 395–414. Berlin/Heidelberg: Springer.
[24] DOI: 10.1007/s001659970003 · Zbl 0966.68124 · doi:10.1007/s001659970003
[25] Latella, D., Majzik, I. and Massink, M. 1999b.Towards a formal operational semantics of UML statechart diagrams, 465Deventer: Kluwer, B.V. · Zbl 0928.68072
[26] Li, W. and Henry, S. 1993.Maintenance metrics for the object-oriented paradigm, 52–60. Washington, DC: IEEE Computer Society Press.
[27] Li, X., Liu, Z. and He, J. 2004.A formal semantics of UML sequence diagrams, 13–16. Melbourne: IEEE Computer Society. April
[28] Lorenz M., Object-oriented software metrics: a practical guide (1994)
[29] McMillan, K.L., 1992. The SMV system, Technical report CMU-CS-92-131, Carnegie Mellon University
[30] Mikk, E. 1998.Implementing statecharts in PROMELA/SPIN, 90Washington, DC: IEEE Computer Society.
[31] NASA, 1995. Software quality metrics for object-oriented system environments. Technical report SATC-TR-95-1001. Greenbelt, MA: National Aeronautics and Space Administration, Goddard Space Flight Center
[32] Ober, I., Graf, S. and Lesens, D. 2006.Modeling and validation of a software architecture for the Ariane-5 launcher, 48–62. Berlin Heidelberg: Springer. Vol. 4037. Lecture Notes in Computer Science
[33] Ober, I., Graf, S. and Ober, I., 2003. Validating timed UML models by simulation and verification. Workshop on Specification and Validation of UML Models for Real Time and Embedded Systems (SVERTS’03), a satellite event of UML 2003, San Francisco, CA, October 2003
[34] OMG, 2006. Systems modeling language (OMG SysML) specification. Technical Report, Object Management Group, Final Adopted Specification of Systems Modeling Language (SysML)
[35] Peled, D. 1994.Combining partial order reductions with on-the-fly model-checking, 377–390. London: Springer-Verlag.
[36] DOI: 10.1007/0-306-48088-3 · doi:10.1007/0-306-48088-3
[37] Störrle, H. 2003.Semantics of Interactions in UML 2.0, 129–136. IEEE Computer Society.
[38] Tugwell, G., et al., 1999. Metrics for full systems engineering lifecycle activities (MeFuSELA). Brighton, UK
[39] Viehl, A. 2006.Formal performance analysis and simulation of UML/SysML models for ESL design, 242–247. Munich: European Design and Automation Association.et al.
[40] Zhan, X. and Miao, H. 2004.An approach to formalizing the semantics of UML statecharts, 753–765. Berlin/Heidelberg: Springer.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.