Partially Introducing Formal Methods into Object-Oriented Development: Case Studies Using a Metrics-Driven Approach

Teaching Coloured Petri Nets - a Gentle Introduction to Formal Methods in a Distributed Systems Course

DAIMI Report Series ◽

10.7146/dpb.v26i520.7049 ◽

1997 ◽

Vol 26 (520) ◽

Author(s):

Søren Christensen ◽

Kjeld Høyer Mortensen

Keyword(s):

Distributed Systems ◽

Petri Nets ◽

Formal Methods ◽

Case Studies ◽

Formal Method ◽

Object Oriented ◽

Coloured Petri Nets ◽

Basic Concepts

This paper is about the two compulsory project assignments set to the students in an undergraduate course on distributed systems. In the first assignment the students design and validate a non-trivial layered protocol by means of Coloured Petri Nets, and in the second they implement the designed protocol in an object-oriented language. From the two assignments the students experience that Coloured Petri Nets, as a formal method, are useful for designing and analysing distributed systems. In the course students are introduced to basic concepts and techniques for distributed systems, and it is explained that such systems are often too complex to manage without using formal methods. In this paper we also report on our experience with teaching the course and describe the didactic methods applied. Based on the obtained experience we conclude that the combination of distributed systems and Coloured Petri Nets is fruitful --- the two areas complement each other. Although our experiences origin in Coloured Petri Nets, we believe that many of our observations hold for other formal methods as well.Topics. Education issues related to nets; Coloured Petri Nets; distributed systems; experience with using nets,case studies; applications of nets to protocols.

Download Full-text

A framework for using formal methods in object-oriented software development

ACM SIGPLAN OOPS Messenger ◽

10.1145/130943.130946 ◽

1992 ◽

Vol 3 (2) ◽

pp. 9-10 ◽

Cited By ~ 2

Author(s):

Richard Holt ◽

Dennis deChampeaux

Keyword(s):

Software Development ◽

Formal Methods ◽

Object Oriented

Download Full-text

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

ACM Transactions on Software Engineering and Methodology ◽

10.1145/3450968 ◽

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.

Download Full-text

Object Normalization as Contribution to the area of Formal Methods of Object-Oriented Database Design

Advances in Computer and Information Sciences and Engineering ◽

10.1007/978-1-4020-8741-7_55 ◽

2008 ◽

pp. 300-304 ◽

Cited By ~ 1

Author(s):

Vojtěch Merunka ◽

Martin Molhanec

Keyword(s):

Formal Methods ◽

Object Oriented ◽

Database Design ◽

Object Oriented Database

Download Full-text

Object-oriented modelling of spacecraft dynamics: tools and case studies

Control-oriented Modelling and Identification: Theory and practice ◽

10.1049/pbce080e_ch10 ◽

2015 ◽

pp. 215-239

Author(s):

Lovera ◽

Casella

Keyword(s):

Case Studies ◽

Object Oriented ◽

Spacecraft Dynamics ◽

Object Oriented Modelling

Download Full-text

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

Software Evolution with UML and XML ◽

10.4018/978-1-59140-462-0.ch004 ◽

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.

Download Full-text

Land Use/Land Cover Assessment over Time Using a New Weighted Environmental Index (WEI) Based on an Object-Oriented Model and GIS Data

Sustainability ◽

10.3390/su122410234 ◽

2020 ◽

Vol 12 (24) ◽

pp. 10234

Author(s):

Javier Rodrigo-Ilarri ◽

Claudia P. Romero ◽

María-Elena Rodrigo-Clavero

Keyword(s):

Land Use ◽

Land Use Change ◽

Land Cover ◽

Case Studies ◽

Object Oriented ◽

Land Use Land Cover ◽

Environmental Index ◽

Land Occupation ◽

Gis Data ◽

Over Time

For the first time, this paper introduces and describes a new Weighted Environmental Index (WEI) based on object-oriented models and GIS data. The index has been designed to integrate all the available information from extensive and detailed GIS databases. After the conceptual definition of the index has been justified, two applications for the regional and local scales of the WEI are shown. The applications analyze the evolution over time of the environmental value from land-use change for two different case studies in Spain: the Valencian Region and the L’Alcora municipality. Data have been obtained from the Spanish Land Occupation Information System (SIOSE) public database and integrate GIS information about land use/land cover on an extensive, high-detailed scale. Results demonstrate the application of the WEI to real case studies and the importance of integrating statistical analysis of WEI evolution over time to arrive at a better understanding of the socio-economic and environmental processes that induce land-use change.

Download Full-text