Abstract
Being part of the systems’ documentation state-based formal specifications can play a crucial role in the software development process. However, besides dense mathematical expressions, their semantical compactness and lack in visually appealing notations impede their use and comprehensibility among different stakeholders. One solution to this problem is to enrich the specification by a semi-formal view, in most cases diagrams with a sufficiently understood semantic meaning. However, as control- and data-dependencies within declarative specifications are hard to detect, existing approaches only cover statics-bearing diagrams. As a way out this paper presents an approach for control- and data dependency analysis within declarative formal specifications. Based on these dependencies, UML diagrams showing static and dynamic properties of the specification are generated.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Laleau, R., Mammar, A.: An overview of a method and its support tool for generating B specifications from uml notations. In; Fiftheenth IEEE Conference on Automated Software Engineering. (2000)
Truong, N.T., Souquieres, J.: An approach for the verification of UML models using B. In: Proceedings of the 11th IEEE Conference and Workshop on the Engineering of Computer-Based Systems (ECBS’04). (2004)
Idani, A., Ledru, Y.: Object oriented concepts identification from formal B specifications. In: Formal Methods in Industrial Critical Applications, FMICS’04. (2004)
Mittermeir, R.T., Bollin, A.: Demand-driven specification partitioning. In: Proceedings of the 5th Joint Modular Languages Conference, JMLC’03. (2003)
Bollin, A.: Maintaining formal specifications. In: Proceedings of the 21st IEEE International Conference on Software Maintenance (ICSM 2005), Budapest, Hungary. (2005) 442–453
Spivey, J.: The Z Notation. C.A.R. Hoare Series. Prentice Hall (1989)
Glass, R.L.: Facts and Fallacies of Software Engineering. Addison-Wesley (2003)
Basili, R.V.: Viewing maintenance as reuse-oriented software development. IEEE Software 7(1) (1990) 19–25
Pirker, H.: Specification based Software Maintenance (a Motivation for Service Channels). PhD thesis, University of Klagenfurt (2001)
Banker, R.D., Davis, G.B., Slaughter, S.A.: Software development practices, software complexity, and software maintenance performance: A field study. In: Management Science. Volume 44., Inst. for Operations Research and the Management Sciences (1998) 433–450
Bollin, A.: Specification Comprehension — Reducing the Complexity of Specifications. PhD thesis, University of Klagenfurt (2004)
Dick, J., Loubersac, J.: A visual approach to VDM: Entity-structure diagrams. Technical Report DE/DRPA/91001, Bull, 68, Route de Versailles, 78430 Louveciennes (France) (1991)
He, X.: PZ Nets-a formal method integrating Petri Nets with Z. Information and Software Technology 43(1) (2001) 1–18
Dupuy, S., Ledru, Y., Chabre-Peccoud, M.: An overview of RoZ: A tool for integrating UML and Z specifications. In: Proceedings of CAiSE’00. (2000) 417–430
Idani, A., Ledru, Y., Bert, D.: Derivation of UML class diagrams as static views of formal B developments. In: 7th International Conference on Formal Engineering Methods, ICFEM 2005. (2005) 37–51
Kim, S.K., Carrington, D.: A formal mapping between UML models and Object-Z specifications. Lecture Notes in Computer Science 1878 (2000) 2–21
Roe, D., Broda, K., Russo, A.: Mapping UML models incorporating OCL constraints into Object-Z. Technical Report ISBN/ISSN: 1469-4174, Imperial College of Science, Technology and Medicine, Department of Computing (2003)
Kim, S.K., Carrington, D.: Visualization of formal specifications. In: In Proceedings Sixth Asia Pacific Software Engineering Conference (ASPEC’99), IEEE Computer. Society Press, Los Alamitos, CA, USA (1999) 102–109
Kent, S.: Constraint diagrams: Visualising invariants in object-oriented models. In: In Proceedings of OOPSLA’97, ACM Press (1997)
Fekih, H., Jemni, L., Merz, S.: Transformation des spècifications B en des diagrammes UML. In: Approches Formelles dans l’Assistance au Développement de Logiciels, AFADL’04, (2004) 131–148
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 International Federation for Information Processing
About this paper
Cite this paper
Bollin, A. (2006). Crossing the Borderline — From Formal to Semi-Formal Specifications. In: Sacha, K. (eds) Software Engineering Techniques: Design for Quality. IFIP International Federation for Information Processing, vol 227. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-39388-9_7
Download citation
DOI: https://doi.org/10.1007/978-0-387-39388-9_7
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-39387-2
Online ISBN: 978-0-387-39388-9
eBook Packages: Computer ScienceComputer Science (R0)