scholarly journals Formal methods into practice: case studies in the application of the B method

1997 ◽  
Vol 144 (2) ◽  
pp. 119 ◽  
Author(s):  
J.C. Bicarregui ◽  
D.L. Clutterbuck ◽  
G. Finnie ◽  
H. Haughton ◽  
K. Lano ◽  
...  
Keyword(s):  
Formal Methods ◽  
Case Studies ◽  
B Method

Practical Formal Methods in Human–Computer Interaction

2018 ◽  
Author(s):  
Alan Dix
Keyword(s):  
Human Computer Interaction ◽  
Computer Science ◽  
Formal Methods ◽  
Case Studies ◽  
Early Development ◽  
Interaction Design ◽  
Formal Training ◽  
Theoretical Interest ◽  
Safety Critical ◽  
Computer Interaction

This chapter explores how precise formal methods can be used effectively and practically in interaction design. The term ‘formal methods’ in computer science refers to a suite of techniques drawing on mathematical notions of sets, logic, and functions or precise diagrammatic notations, most of which are currently primarily focused on safety-critical applications in the aerospace or nuclear industries. While research into broader use of these methods could be regarded as a theoretical interest, the early development of formal methods was driven as much by practical considerations as theory. This chapter features two case studies on formal notations and their use in areas of practical interaction design beyond safety-critical applications, as well as understood, used, and appropriated by clients and designers who have no formal training or expertise. Each offers specific notations and techniques to the reader and also explores more general lessons for creating practical formal methods for HCI.

scholarly journals Coloured Petri Nets - a Pragmatic Formal Method for Designing and Analysing Distributed Systems

1997 ◽  
Vol 26 (522) ◽  
Author(s):  
Kjeld Høyer Mortensen
Keyword(s):  
Formal Methods ◽  
Case Studies ◽  
Formal Method ◽  
Attractive Alternative ◽  
Coloured Petri Nets ◽  
Domain Specific ◽  
Language Constructs ◽  
Representative Selection ◽  
Phd Thesis ◽  
Selection Of

<p>The thesis consists of six <em>individual</em> papers, where the present paper contains the mandatory overview, while the remaining five papers are found separately from the overview. The five papers can roughly be divided into three areas of research, namely case studies, education, and extensions to the CPN method.</p><p>The primary purpose of the PhD thesis is to study the pragmatics, practical aspects, and intuition of CP-nets viewed as a formal method for describing and reasoning about concurrent systems. The perspective of pragmatics is our leitmotif, but at the same time in the context of CP-nets it is a kind of hypothesis of this thesis. This overview paper summarises the research conducted as an investigation of the hypothesis in the three areas of case studies, education, and extensions.</p><p>The provoking claim of pragmatics should not be underestimated. In the present overview of the thesis, the CPN method is compared with a representative selection of formal methods. The graphics and simplicity of semantics, yet generality and expressiveness of the language constructs, essentially makes CP-nets a viable and attractive alternative to other formal methods. Similar graphical formal methods, such as SDL and Statecharts, typically have significantly more complicated semantics, or are domain-specific languages.</p><p>research conducted in this thesis, opens a new complex of problems. Firstly, to get wider acceptance of CP-nets in industry, it is important to identify fruitful areas for the effective introduction of the CPN method. Secondly, it would be useful to identify a few extensions to the CPN method inspired by specific domains for easier adaption in industry. Thirdly, which analysis methods do future systems make use of?</p>

scholarly journals Early Validation of Functional Requirements and Transition to Source Code with Event-B

2020 ◽  
Author(s):  
Nestor Cataño
Keyword(s):  
Formal Methods ◽  
Case Studies ◽  
Code Generation ◽  
Lessons Learned ◽  
Functional Requirements ◽  
Alternative Approach ◽  
Early Validation ◽  
To Come ◽  
The Cost ◽  
Automated Code Generation

The cost of fixing software requirements errors after deployment is so high that it is vital to come up with ways to find and fix requirements errors early in the life-cycle of a project. The work in this paper advocates for the use of formal methods as an alternative approach to guarantee the correctness of the software from requirements to code. We present a formal-methods based approach for the early validation of functional requirements. Our approach relies on formal methods techniques such as program refinement, correctness-by-construction (CbyC), and automated code generation. We present two case studies that showcase our approach; for the case studies, we discuss design decisions, flaws encountered, and lessons learned.

The Rational Deterrence Debate

1989 ◽  
Vol 41 (2) ◽  
pp. 225-237 ◽  
Author(s):  
George W. Downs
Keyword(s):  
Formal Methods ◽  
Case Studies ◽  
Strategic Behavior ◽  
The Other ◽  
Heuristics And Biases ◽  
Deterrence Theory ◽  
Rational Theory ◽  
Other Hand ◽  
The World

Although there are important differences between the rational theory of deterrence and the theory of deterrence that is emerging from the psychology and case-study literatures, it is necessary for adherents of both to appreciate the ways in which they complement each other and the problems they share. For example, rational deterrence theory will not describe the way the world works until certain heuristics and biases that can only be discovered through case studies and other inferential methods are either eliminated or integrated into the theory. On the other hand, psychologists and case-study researchers will find it difficult to trace through the implications of their discoveries for strategic behavior until they adopt some relative of formal methods.

‘Enigmatic Images from Remote Prehistory’

2017 ◽  
Author(s):  
Andrew Meirion Jones ◽  
Marta Díaz-Guardamino
Keyword(s):  
North America ◽  
Formal Methods ◽  
Case Studies ◽  
Rock Art ◽  
Hierarchical Approach ◽  
Relational Approach ◽  
Ontological Priority ◽  
Art Analysis

This chapter explores questions of ontology in rock art analysis. More specifically, it argues that the distinction between ‘informed’ methods and ‘formal’ methods reproduces some problematic dichotomies, such as the distinction between active subjects and inert objects, culture and nature, and a conceptualization of meaning as being external to the art itself. The chapter proposes a move away from such an ontologically hierarchical approach to rock art analysis to a relational approach in which there is no ontological priority between the different elements that make up the rock art assemblage. It emphasizes that placing formal methods at the heart of rock art studies, alongside analogy, shifts the questions we ask of rock art away from simple epistemologically derived enquiries to ontological questions. To illustrate this the chapter examines case studies of parietal art of the European Palaeolithic and Comanche rock art in North America.

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

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

<p>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.</p><p><strong>Topics.</strong> Education issues related to nets; Coloured Petri Nets; distributed systems; experience with using nets,case studies; applications of nets to protocols.</p>

Corporate Sustainability: Challenge to Managerial Orthodoxies

2003 ◽  
Vol 9 (1) ◽  
pp. 2-11 ◽  
Author(s):  
Dexter Dunphy
Keyword(s):  
Case Studies ◽  
Corporate Sustainability ◽  
Central Place ◽  
Marked Contrast ◽  
Sustainability Management

ABSTRACTThis paper addresses the issue of corporate sustainability. It examines why achieving sustainability is becoming an increasingly vital issue for society and organisations, defines sustainability and then outlines a set of phases through which organisations can move to achieve increasing levels of sustainability. Case studies are presented of organisations at various phases indicating the benefits, for the organisation and its stakeholders, which can be made at each phase. Finally the paper argues that there is a marked contrast between the two competing philosophies of neo-conservatism (economic rationalism) and the emerging philosophy of sustainability. Management schools have been strongly influenced by economic rationalism, which underpins the traditional orthodoxies presented in such schools. Sustainability represents an urgent challenge for management schools to rethink these traditional orthodoxies and give sustainability a central place in the curriculum.

Sign in / Sign up

Export Citation Format

Share Document