A Case Study in the Formal Modeling of Safe and Secure Manufacturing Automation

Computer ◽  
2021 ◽  
Vol 54 (9) ◽  
pp. 59-71
Author(s):  
Matthew Jablonski ◽  
Bo Yu ◽  
Gabriela Felicia Ciocarlie ◽  
Paulo Costa
Keyword(s):  
Formal Modeling ◽  
Manufacturing Automation

scholarly journals Formal Modeling and Analysis of Fairness Characterization of E-Commerce Protocols

2014 ◽  
Vol 2014 ◽  
pp. 1-10
Author(s):  
Chengwei Zhang ◽  
Xiaohong Li ◽  
Jing Hu ◽  
Zhiyong Feng ◽  
Jiaojiao Song
Keyword(s):  
Formal Modeling ◽  
Sufficient Condition ◽  
Formal Approach ◽  
Common Assumption ◽  
Modeling And Analysis ◽  
Verification Method ◽  
Space Model ◽  
The Past

In the past, fairness verification of exchanges between the traders in E-commerce was based on a common assumption, so-called nonrepudiation property, which says that if the parties involved can deny that they have received or sent some information, then the exchanging protocol is unfair. So, the nonrepudiation property is not a sufficient condition. In this paper, we formulate a new notion of fairness verification based on the strand space model and propose a method for fairness verification, which can potentially determine whether evidences have been forged in transactions. We first present an innovative formal approach not to depend on nonrepudiation, and then establish a relative trader model and extend the strand space model in accordance with traders’ behaviors of E-commerce. We present a case study to demonstrate the effectiveness of our verification method.

Formal Modeling and Validation Applied to a Commercial Coherent Bus: A Case Study

1997 ◽  
pp. 48-62 ◽  
Author(s):  
Ganesh Gopalakrishnan ◽  
Rajnish Ghughal ◽  
Ravi Hosabettu ◽  
Abdelillah Mokkedem ◽  
Ratan Nalumasu
Keyword(s):  
Formal Modeling

The National Shipbuilding Research Program, 1971-1976

1976 ◽  
Vol 13 (04) ◽  
pp. 371-380
Author(s):  
John J. Garvey
Keyword(s):  
Federal Government ◽  
Research Program ◽  
Material Handling ◽  
Innovation Process ◽  
Government Subsidy ◽  
Shipbuilding Industry ◽  
Production Methods ◽  
Manufacturing Automation ◽  
The Government

This paper is a description of the organization and operation of a unique research program sponsored by the Federal Government in full partnership with the U. S. shipbuilding industry. The objective of the program is to improve the productivity of this industry and to reduce Government subsidy. Since the program began in 1971, almost 90 projects have been funded by the Government at a cost of $15 million. In addition, the industry has contributed in manpower, material, and facilities in excess of $5 million. The bulk of the projects involve development and demonstration of production technology for shipbuilding. These include welding, material handling, ship outfitting, production methods, manufacturing automation, and production-oriented design. In addition to describing the technical and organizational content of the program, the paper is intended to be a case study of a successful government/industry approach to improve the total innovation process within a mature industry.

Formal modeling and analysis of resource management for cloud architectures: an industrial case study using Real-Time ABS

2013 ◽  
Vol 8 (4) ◽  
pp. 323-339 ◽  
Author(s):  
Elvira Albert ◽  
Frank S. de Boer ◽  
Reiner Hähnle ◽  
Einar Broch Johnsen ◽  
Rudolf Schlatte ◽  
...  
Keyword(s):  
Resource Management ◽  
Real Time ◽  
Formal Modeling ◽  
Industrial Case Study ◽  
Modeling And Analysis

scholarly journals Towards Practical Guidelines for Conversion from Fixed to Reconfigurable Manufacturing Automation Systems

2018 ◽  
Vol 03 (01) ◽  
pp. 1850002 ◽  
Author(s):  
Alan Coppini ◽  
Michael A. Saliba
Keyword(s):  
Manufacturing System ◽  
Economic Feasibility ◽  
Reconfigurable Manufacturing ◽  
Reconfigurable Manufacturing System ◽  
Manufacturing Automation ◽  
Reconfigurable System ◽  
Automation Systems ◽  
Practical Guidelines ◽  
Manufacturing Machine

It is generally considered that economic feasibility of a reconfigurable manufacturing system (RMS) is only attainable if the system is defined to be reconfigurable at the outset of its design. In this work, we consider the potential exception to this perception, in the context of a common industrial scenario where a specialized and expensive manufacturing machine or system will otherwise be rendered useless due to the loss of business of the particular product being manufactured. Specific guidelines to convert from a fixed to a reconfigurable system are proposed, and evaluated through a case study. It is shown that under certain conditions, RMSs may be economically feasible even if they are developed through the modification of pre-existing dedicated systems.

Formal Modeling of Resource Management for Cloud Architectures: An Industrial Case Study

2012 ◽  
pp. 91-106 ◽  
Author(s):  
Frank S. de Boer ◽  
Reiner Hähnle ◽  
Einar Broch Johnsen ◽  
Rudolf Schlatte ◽  
Peter Y. H. Wong
Keyword(s):  
Resource Management ◽  
Formal Modeling ◽  
Industrial Case Study

Applicability of generalized test tables: a case study using the manufacturing system demonstrator xPPU

2018 ◽  
Vol 66 (10) ◽  
pp. 834-848 ◽  
Author(s):  
Suhyun Cha ◽  
Alexander Weigl ◽  
Mattias Ulbrich ◽  
Bernhard Beckert ◽  
Birgit Vogel-Heuser
Keyword(s):  
Production Systems ◽  
Reactive Systems ◽  
Internal Variables ◽  
High Coverage ◽  
Manufacturing Automation ◽  
Automated Production ◽  
Recent Trends ◽  
Requirements Quality ◽  
Automation Control

Abstract With recent trends in manufacturing automation, control software in automated production systems becomes more complex and has more variability to keep pace with customer and market requirements. Quality assurance also becomes more and more important to ensure that the systems live up to expectations. However, correctness of automation software is rarely verified using formal techniques in spite of their high coverage. One of the main reasons is the lack of specification languages suitable for this application area that are both comprehensible and sufficiently expressive. Generalized test tables (GTTs), which are a specification language for reactive systems, were presented recently as an accessible representation for application engineers. This formalism achieves both the comprehensibility of concrete test tables and the coverage of formal methods. In our approach, the specification provided by GTTs is used for formal verification, especially model checking. In this paper, we present four new features for GTTs: the progression flag, strong repetition, row grouping, and specification on internal variables. We demonstrate the applicability and evaluate the comprehensibility of GTT-based specification and verification using a range of diverse scenarios from the community demonstrator, the extended Pick & Place Unit.

Sign in / Sign up

Export Citation Format

Share Document