Abstract
SysML is a UML-based graphical notation for systems engineering that is becoming a de facto standard. Whilst it reuses a number of UML diagrams, it introduces new diagrams, and maintains the loose UML semantics. Refinement is a formal technique that supports the validation and verification of models by capturing a notion of correctness based on observable behaviour. In this paper, we analyse the issue of formal refinement in the context of SysML. First, we identify the requirements for supporting refinement in SysML, next we propose extensions to SysML that satisfy these requirements, and finally we present a few refinement laws and discuss their validity.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
OMG: OMG Systems Modeling Language (OMG SysMLTM). Technical report, OMG Document Number: formal/2010-06-02 (2010)
Rational Rhapsody Architect for Systems Engineers, http://tinyurl.com/rrafse (accessed April 11, 2013)
Artisan Studio, http://atego.com/products/artisan-studio/ (accessed April 11, 2013)
Sparx Systems’ Enterprise Architect supports the Systems Modeling Language, http://www.sparxsystems.com/products/mdg/tech/sysml (accessed April 11, 2013)
Miyazawa, A., Lima, L., Cavalcanti, A.: Formal models of sysml blocks. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 249–264. Springer, Heidelberg (2013)
Lima, L., Didier, A., Cornélio, M.: A Formal Semantics for SysML Activity Diagrams. In: Iyoda, J., de Moura, L. (eds.) SBMF 2013. LNCS, vol. 8195, pp. 179–194. Springer, Heidelberg (2013)
Albertins, L., Cavalcanti, A., Cornélio, M., Iyoda, J., Miyazawa, A., Payne, R.: Final Report on Combining SysML and CML. Technical Report D22.4, COMPASS Deliverable (March 2013)
Fitzgerald, J., Larsen, P.G.: Modelling Systems – Practical Tools and Techniques in Software Development, 2nd edn. Cambridge University Press (2009)
Hoare, C.A.R.: Communicating sequential processes. Prentice-Hall, Inc. (1985)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall Series in Computer Science. Prentice-Hall, New York (1998)
Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice Hall International Series in Computer Science (1994)
Hoare, T., Jifeng, H.: Unifying Theories of Programming. Prentice Hall (1998)
Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: A Refinement Strategy for Circus. Formal Aspects of Computing 15(2-3), 146–181 (2003)
Correa, N., Giandini, R.: A UML extension to specify model refinements. In: XXXII Latin American Conference on Informatics (2006)
Pons, C., Perez, G., Giandini, R., Kutsche, R.D., TU-Berlin, F.: Understanding Refinement and Specialization in the UML. In: 2nd International Workshop on MAnaging SPEcialization/Generalization Hierarchies (MASPEGHI) (2003)
Pons, C.: On the definition of UML refinement patterns. In: 2nd MoDeVa Workshop, Model Design and Validation. ACM/IEEE (2005)
Bergner, K., Rausch, A., Sihling, M., Vilbig, A.: Structuring and refinement of class diagrams. In: Proc. of the 32nd Annual Hawaii International Conference on Systems Sciences. IEEE (1999)
Hnatkowska, B., Huzar, Z., Kuźniarz, L., Tuzinkiewicz, L.: On understanding of refinement relationship. In: Consistency Problems in UML-based Software Development: Understanding and Usage of Dependency (2004)
Liu, Z., Li, X., Liu, J., Jifeng, H.: Consistency and refinement of UML models. In: Consistency Problems in UML-based Software Development: Understanding and Usage of Dependency (2004)
Van Der Straeten, R.: Formalizing Behaviour Preserving Dependencies in UML. In: Consistency Problems in UML-Based Software Development: Understanding and Usage of Dependency (2004)
Said, M.Y., Butler, M., Snook, C.: Class and state machine refinement in UML-B. In: Proc. of Workshop on Integration of Model-Based Formal Methods and Tools (2009)
Davies, J., Crichton, C.: Concurrency and refinement in the unified modeling language. Formal Aspects of Computing 15(2-3), 118–145 (2003)
Woodcock, J., Cavalcanti, A., Coleman, J., Didier, A., Larsen, P.G., Miyazawa, A., Oliveira, M.: CML Definition 0. Technical Report D23.1, COMPASS Deliverable (June 2012)
Miyazawa, A., Cavalcanti, A., Foster, S.: Refinement in SysML and CML. Technical report, Department of Computer Science, The University of York (2014), http://cs.york.ac.uk/~alvarohm/report2014a.pdf
OMG: OMG Unified Modeling Language (OMG UML), superstructure, version 2.4.1. Technical report (2011)
Abrial, J.R.: The Event-B Modelling Notation (October 2007)
Bryans, J., Fitzgerald, J., Payne, R., Miyazawa, A., Kristensen, K.: SysML Contracts for Systems of Systems. In: Proc. of the 9th International Conference on Systems of Systems Enginering (2014)
Foster, S., Payne, R., Couto, L.D.: Towards Verification of Constituent Systems through Automated Proof. In: Proc. of the Workshop on Engineering Dependable Systems of Systems (EDSoS) (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Miyazawa, A., Cavalcanti, A. (2014). Formal Refinement in SysML. In: Albert, E., Sekerinski, E. (eds) Integrated Formal Methods. IFM 2014. Lecture Notes in Computer Science(), vol 8739. Springer, Cham. https://doi.org/10.1007/978-3-319-10181-1_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-10181-1_10
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10180-4
Online ISBN: 978-3-319-10181-1
eBook Packages: Computer ScienceComputer Science (R0)