scholarly journals Using lightweight formal methods to model class and object diagrams

2012 ◽  
Vol 9 (1) ◽  
pp. 411-429
Author(s):  
Fernando Valles-Barajas
Keyword(s):  
Formal Methods ◽  
Formal Method ◽  
Formal Model ◽  
Modeling Language ◽  
Form Class ◽  
Software Models ◽  
Proposed Model ◽  
Model Class ◽  
Lightweight Formal Methods

In this paper a formal model for class and object diagrams is presented. To make the model the author used Alloy, which is a threein-one package: a modeling language that constructs software models, a formal method that guides the construction of software models and an analyzer that helps find inconsistencies in software models. In the proposed model the entities that form class and object diagrams, as well as the rules that govern how these elements can be connected, are specified.

Specifying with Interface and Trait Abstractions in Abstract State Machines: A Controlled Experiment

2021 ◽  
Vol 30 (4) ◽  
pp. 1-29
Author(s):  
Philipp Paulweber ◽  
Georg Simhandl ◽  
Uwe Zdun
Keyword(s):  
Formal Methods ◽  
Formal Method ◽  
Object Oriented ◽  
Controlled Experiment ◽  
Specification Languages ◽  
Randomized Design ◽  
Textual Description ◽  
Efficiency And Effectiveness ◽  
Completely Randomized Design ◽  
Experimental Group

Abstract State Machine (ASM) theory is a well-known state-based formal method. As in other state-based formal methods, the proposed specification languages for ASMs still lack easy-to-comprehend abstractions to express structural and behavioral aspects of specifications. Our goal is to investigate object-oriented abstractions such as interfaces and traits for ASM-based specification languages. We report on a controlled experiment with 98 participants to study the specification efficiency and effectiveness in which participants needed to comprehend an informal specification as problem (stimulus) in form of a textual description and express a corresponding solution in form of a textual ASM specification using either interface or trait syntax extensions. The study was carried out with a completely randomized design and one alternative (interface or trait) per experimental group. The results indicate that specification effectiveness of the traits experiment group shows a better performance compared to the interfaces experiment group, but specification efficiency shows no statistically significant differences. To the best of our knowledge, this is the first empirical study studying the specification effectiveness and efficiency of object-oriented abstractions in the context of formal methods.

scholarly journals Dependability Modeling and Assessment in UML-Based Software Development

2012 ◽  
Vol 2012 ◽  
pp. 1-11 ◽  
Author(s):  
Simona Bernardi ◽  
José Merseguer ◽  
Dorina C. Petriu
Keyword(s):  
Software Development ◽  
Formal Model ◽  
General Purpose ◽  
Software Modeling ◽  
Model Driven ◽  
Domain Specific ◽  
Software Model ◽  
Software Models ◽  
Assessment Approach ◽  
System Properties

Assessment of software nonfunctional properties (NFP) is an important problem in software development. In the context of model-driven development, an emerging approach for the analysis of different NFPs consists of the following steps: (a) to extend the software models with annotations describing the NFP of interest; (b) to transform automatically the annotated software model to the formalism chosen for NFP analysis; (c) to analyze the formal model using existing solvers; (d) to assess the software based on the results and give feedback to designers. Such a modeling→analysis→assessment approach can be applied to any software modeling language, be it general purpose or domain specific. In this paper, we focus on UML-based development and on the dependability NFP, which encompasses reliability, availability, safety, integrity, and maintainability. The paper presents the profile used to extend UML with dependability information, the model transformation to generate a DSPN formal model, and the assessment of the system properties based on the DSPN results.

Towards the Integration of a Formal Object-Oriented Method and Relational Unified Process

2011 ◽  
pp. 101-133
Author(s):  
Jing Liu ◽  
Zhiming Lui ◽  
Xiaoshan Li ◽  
He Jifend ◽  
Yifeng Chen
Keyword(s):  
Formal Methods ◽  
Formal Method ◽  
System Development ◽  
Scale Up ◽  
Object Oriented ◽  
Use Case ◽  
Object Oriented Method ◽  
Unified Process ◽  
Sound Foundation

In this chapter, we study the use of a formal object-oriented method within Relational Unified Process (RUP). Our purposes are (a) to unify different views of UML models; (b) to enhance RUP and UML with a formal method to improve the quality of software; (c) to scale up the use of the formal method with the use-case driven, iterative and incremental aspects of RUP. Our overall aim is to establish a sound foundation of RUP and UML and scale up the use of formal methods in software-intensive system development.

Seamless Formalizing the UML Semantics through Metamodels

2001 ◽  
pp. 225-249 ◽  
Author(s):  
Jose Luis Fernandez Aleman ◽  
Ambrosio Toval Alvarez
Keyword(s):  
Formal Model ◽  
Language Evolution ◽  
Formal Semantics ◽  
Unified Modeling Language ◽  
Modeling Language ◽  
Algebraic Specification ◽  
Unified Modeling ◽  
Management Group ◽  
Specification Theory ◽  
Insight Into

Despite the fact that the Unified Modeling Language (UML) has been adopted by the Object Management Group (OMG2 ) as the standard notation for use in Object-Oriented (OO) Systems Development, it still does not have a truly formal semantics. There is currently much effort directed towards formalizing particular aspects or models of UML. However, the literature gives little insight into the appropriate strategy for tackling this problem within an integrated basis including the language evolution. This chapter identifies and discusses three feasible strategies which can be applied to formalize UML. One of these strategies is selected to underpin the four-layer architecture on which UML is based. The approach is based on the soundness of algebraic specification theory, which, in addition, provides suitable theorem-proving capabilities for exploiting the UML formal model obtained. The formal models proposed are specified using an executable algebraic specification language called Maude.

scholarly journals Revising Probabilities and Full Beliefs

2020 ◽  
Vol 49 (5) ◽  
pp. 1005-1039 ◽  
Author(s):  
Sven Ove Hansson
Keyword(s):  
Formal Model ◽  
Belief Change ◽  
Learning From Experience ◽  
Epistemic Agent ◽  
Set Operations ◽  
Proposed Model ◽  
Formal Properties ◽  
Belief States ◽  
Do So ◽  
Belief Set

Abstract A new formal model of belief dynamics is proposed, in which the epistemic agent has both probabilistic beliefs and full beliefs. The agent has full belief in a proposition if and only if she considers the probability that it is false to be so close to zero that she chooses to disregard that probability. She treats such a proposition as having the probability 1, but, importantly, she is still willing and able to revise that probability assignment if she receives information that gives her sufficient reasons to do so. Such a proposition is (presently) undoubted, but not undoubtable (incorrigible). In the formal model it is assigned a probability 1 − δ, where δ is an infinitesimal number. The proposed model employs probabilistic belief states that contain several underlying probability functions representing alternative probabilistic states of the world. Furthermore, a distinction is made between update and revision, in the same way as in the literature on (dichotomous) belief change. The formal properties of the model are investigated, including properties relevant for learning from experience. The set of propositions whose probabilities are infinitesimally close to 1 forms a (logically closed) belief set. Operations that change the probabilistic belief state give rise to changes in this belief set, which have much in common with traditional operations of belief change.

A New Formal Method of Anticorrosion Design

2010 ◽  
Vol 44-47 ◽  
pp. 1449-1454 ◽  
Author(s):  
Peng Fei Zhao ◽  
Yi Zhang ◽  
Zong Bin Li ◽  
Xiao Yang Yuan
Keyword(s):  
Conceptual Design ◽  
Formal Method ◽  
Formal Model ◽  
Early Stage ◽  
Formal Description ◽  
Functional Requirements ◽  
Formal Reasoning ◽  
Sets Theory ◽  
Polychromatic Sets Theory ◽  
Selection Of

To solve the problem of anticorrosion design in early stage of manufacture, a formal method of anticorrosion design was proposed, and a formal model of conceptual design of anticorrosive materials was established by using hierarchical structure, individual color sets and unified color sets. Basing on the reasoning matrices which were established by using polychromatic sets theory, a formal reasoning method was proposed to realize the formal reasoning from the functional requirements to the selection of final scheme. This formal method of conceptual design for anticorrosion based on the polychromatic sets can make the design process of anticorrosion standardized, and facilitate the formal description of the reasoning process and its expression and operation in computer. The method made some useful explorationfor the CAPP integration design of anticorrosion.

Utilization of Concept Selection Methods: A Survey of Finnish Industry

2005 ◽  
Author(s):  
Mikko Salonen ◽  
Matti Perttula
Keyword(s):  
Formal Methods ◽  
Design Research ◽  
Formal Method ◽  
Formal Concept ◽  
Concept Design ◽  
Selection Methods ◽  
Concept Selection ◽  
Analytic Hierarchy ◽  
Industrial Utilization ◽  
Concept Review

Concept selection is an area of design research that has been under considerable interest over the years. There is, however, only little information on how the methods that have been presented in design research for this task have been adopted by industry. Thus, a survey was carried out in the Finnish industry. The results revealed that the degree of industrial utilization of formal concept selection methods was relatively low. Less than one out of four companies responded to use one or several of the formal methods included in the study: Pugh’s evaluation matrix, Rating matrices, or Analytic Hierarchy Process (AHP). Concept review meeting were reported as the most common approach for concept selection. However, a majority of the companies that did not utilize any formal method reported lacking effective and suitable methods for concept selection. The companies using formal methods were more satisfied. The first conclusion from the study is that there is a basis for a higher degree of utilization of formal concept selection methods in industry. Our second conclusion is that the existing formal concept selection methods do not entirely fulfill the needs of concept selection in an industry context. We propose that numerical concept selection methods should be further developed and extended to better support the decision-making practices of concept selection in industry. This type of concept selection is characterized by the participation of multiple decision makers through concept design reviews.

sMML - A Smart MetaModeling Language for Flexible Modeling

2005 ◽  
Vol 17 (1) ◽  
pp. 3-10 ◽  
Author(s):  
Makoto Oya ◽  
Keyword(s):  
Systems Design ◽  
General Purpose ◽  
Modeling Language ◽  
Modeling Languages ◽  
Software Designers ◽  
Flexible Modeling ◽  
Software Models ◽  
Custom Made ◽  
Wide Range ◽  
Application Specific

Modeling is the key to software design, from large information systems to embedded software. Without well-considered software models, the developed implementation becomes inconsistent or distant from the original requirement. A model is created using a modeling language. UML is a standardized general-purpose modeling language widely used in enterprise systems design. Because it is very large language, UML is not always appropriate for designing small software. Designers also often want to describe models differently based on the immediate need preferring simple, application-specific but flexible notation rather than the rigidity of UML. We propose a metamodeling language, called <I>sMML</I>, to define custom-made modeling language that enables designers to define a suitable modeling language on demand, then write actual models using it. <I>sMML</I> is a metamodeling language small enough to define a variety of modeling languages, self-closed and independent of other modeling languages, and aligned with UML. After completely defining <I>sMML</I>, we present experimental results applying <I>sMML</I>, taking a simple modeling language and UML as examples, which demonstrates that <I>sMML</I> is useful for flexible modeling and capable of defining a wide range of modeling languages.

Sign in / Sign up

Export Citation Format

Share Document