scholarly journals A LTS Approach to Control in Event-B

2018 ◽  
Vol 2018 ◽  
pp. 1-11 ◽  
Author(s):  
Han Peng ◽  
Chenglie Du ◽  
Lei Rao ◽  
Fu Chen
Keyword(s):  
Flow Model ◽  
State Machine ◽  
Transition System ◽  
Control Flow ◽  
Behavior Modeling ◽  
System Model ◽  
Behavior Model ◽  
System Behavior ◽  
Labeled Transition System ◽  
Event Trace

In Event-B, people need to use control variables to constrain the order of events, which is a time-consuming and error-prone process. This paper presents a method of combining labeled transition system and iUML-B to complete the behavior modeling of system, which is more convenient and practical for engineers who are accustomed to using the automaton to build a system behavior model. First, we use labeled transition system to establish the behavior model of the system. Then we simulate and verify the event traces of the labeled transition system behavior model. Finally, we convert labeled transition system model into iUML-B state machine and use it to generate the corresponding control flow model. We use Abrial’s bounded retransmission protocol to demonstrate the practicality of our approach. The simulation results show that the system behavior model generated by the iUML-B state machine has the same event trace as the corresponding labeled transition system model.

Fuzzy Labeled Transition Refinement Tree

2014 ◽  
Vol 6 (3) ◽  
pp. 1-31 ◽  
Author(s):  
Sofia Kouah ◽  
Djamel-Eddine Saidouni
Keyword(s):  
Dynamic Systems ◽  
Transition System ◽  
System Model ◽  
Design Parameters ◽  
Concurrent Design ◽  
Incremental Development ◽  
Action Refinement ◽  
Formal Framework ◽  
Labeled Transition System ◽  
Multi Agents

This paper aims to provide a formal framework that supports an incremental development of dynamic systems such as multi agents systems (MAS). We propose a fuzzy labeled transition system model (FLTS for short). FLTS allows a concise action refinement representation and deals with incomplete information through its fuzziness representation. Afterward, based on FLTS model, we propose a refinement model called fuzzy labeled transition refinement tree (FLTRT for short). The FLTRT structure serves as a tree of potential concurrent design trajectories of the system. Also, we introduce bisimulation relations for both models in order to identify equivalent design trajectories, which could be assessed with respect to relevant design parameters.

Fuzzy Labeled Transition Refinement Tree

Fuzzy Systems ◽  
2017 ◽  
pp. 873-905 ◽  
Author(s):  
Sofia Kouah ◽  
Djamel-Eddine Saidouni
Keyword(s):  
Incomplete Information ◽  
Dynamic Systems ◽  
Transition System ◽  
System Model ◽  
Design Parameters ◽  
Concurrent Design ◽  
Incremental Development ◽  
Action Refinement ◽  
Formal Framework ◽  
Labeled Transition System

This paper aims to provide a formal framework that supports an incremental development of dynamic systems such as multi agents systems (MAS). We propose a fuzzy labeled transition system model (FLTS for short). FLTS allows a concise action refinement representation and deals with incomplete information through its fuzziness representation. Afterward, based on FLTS model, we propose a refinement model called fuzzy labeled transition refinement tree (FLTRT for short). The FLTRT structure serves as a tree of potential concurrent design trajectories of the system. Also, we introduce bisimulation relations for both models in order to identify equivalent design trajectories, which could be assessed with respect to relevant design parameters.

System Behavior Modeling As a Basis for Advanced Failure Modes and Effects Analysis

1996 ◽  
Author(s):  
Charles F. Eubanks ◽  
Steven Kmenta ◽  
Kosuke Ishii
Keyword(s):  
Conceptual Design ◽  
Failure Modes ◽  
Behavior Modeling ◽  
Behavior Model ◽  
System Behavior ◽  
Early Stages ◽  
Device Operation

Abstract This paper presents a method for developing a device behavior model to enhance reliability at the early stages of conceptual design. The model facilitates a semi-automated advanced failure modes and effects analysis (FMEA). The model performs analyses and simulations of device behavior, reasons about conditions that depart from desired behaviors, and analyzes the results of those departures. The proposed method rigorously specifies pre- and post-conditions, yet is flexible in the syntax of device operation. The paper shows how the method can capture failures normally missed by existing FMEA methods. An automatic ice maker serves as an example application.

Developing Intelligent Semantic Web Services

2011 ◽  
pp. 422-438
Author(s):  
Sam Lee
Keyword(s):  
Web Services ◽  
Semantic Web ◽  
Code Generation ◽  
Intelligent Agent ◽  
Semantic Web Services ◽  
Behavior Model ◽  
System Behavior ◽  
Heterogeneous Information ◽  
High Degree ◽  
The Web

This chapter introduces an approach to the development of intelligent Semantic Web services, which are envisioned as system cells that actively discover, learn, and communicate knowledge on the Web. The development of these systems often involves not only standardized Web technology, but also the integration of heterogeneous information. The approach in this chapter adopts the Semantic Web services specifications that are given by the DARPA agent markup language (DAML) program, utilizes a system behavior model to represent an intelligent agent, and proposes a high degree of automatic synthesis using code generation and program templates. The author reviews the various techniques that are available to aid the development process, and provides an example to illustrate the stages of software synthesis in the development of such systems.

Research on Behavior Modeling and Simulation of Complex UAV Based on SysML State Machine Diagram

2021 ◽  
pp. 401-409
Author(s):  
Yuanjie Lu ◽  
Zhimin Liu ◽  
Zhixiao Sun ◽  
Miao Wang ◽  
Wenqing Yi ◽  
...  
Keyword(s):  
Modeling And Simulation ◽  
State Machine ◽  
Behavior Modeling ◽  
State Machine Diagram

Hierarchical Design Method for Multi-Agent Systems

2015 ◽  
Vol 7 (2) ◽  
pp. 105-134
Author(s):  
Bouneb Messaouda ◽  
Saïdouni Djamel Eddine
Keyword(s):  
Design Methodology ◽  
Design Method ◽  
Transition System ◽  
Hierarchical Design ◽  
Multi Agent Systems ◽  
Agent Systems ◽  
Multi Agent ◽  
Labeled Transition System ◽  
System Assessment ◽  
Definition Of

This paper proposes a new hierarchical design method for the specification and the verification of multi agent systems (MAS). For this purpose, the authors propose the model of Refinable Recursive Petri Nets (RRPN) under a maximality semantics. In this model, a notion of undefined transitions is considered. The underlying semantics model is the Abstract Maximality-based Labeled Transition System (AMLTS). Hence, the model supports a definition of a hierarchical design methodology. The example of goods transportation is used for illustrating the approach. For the system assessment, the properties are expressed in CTL logic and verified using the verification environment FOCOVE (Formal Concurrency Verification Environment).

Application of Fuzzy Labeled Transition System to Contract Net Protocol

2015 ◽  
Vol 6 (3) ◽  
pp. 27-46 ◽  
Author(s):  
Sofia Kouah ◽  
Djamel Eddine Saïdouni
Keyword(s):  
Dynamic Systems ◽  
Transition System ◽  
Multi Agent Systems ◽  
Contract Net Protocol ◽  
Agent Systems ◽  
Contract Net ◽  
Multi Agent ◽  
Refinement Process ◽  
Labeled Transition System

For developing large dynamic systems in a rigorous manner, fuzzy labeled transition refinement tree (FLTRT for short) has been defined. This model provides a formal specification framework for designing such systems. In fact, it supports abstraction and enables fuzziness which allows a rigorous formal refinement process. The purpose of this paper is to illustrate the applicability of FLTRT for designing multi agent systems (MAS for short), among others collective and internal agent's behaviors. Therefore, Contract Net Protocol (CNP for short) is chosen as case study.

scholarly journals The Importance of Validating Sleep Behavior Models for Fatigue Management Software in Military Aviation

2020 ◽  
Vol 185 (11-12) ◽  
pp. e1986-e1991 ◽  
Author(s):  
Michel A Paul ◽  
Steven R Hursh ◽  
Ryan J Love
Keyword(s):  
Target Population ◽  
Behavior Modeling ◽  
Behavior Model ◽  
Canadian Forces ◽  
Sleep Behavior ◽  
Specific Target ◽  
Commute Time ◽  
Harmonization Process ◽  
Scheduling Tool ◽  
Behavior Models

Abstract Introduction The propensity for air mobility missions to exhaust aircrews is strongly dependent on operational tempo. Most flying is performed during periods of low to moderate operational tempo, but a major flight safety risk can emerge when operational tempo becomes very high. This risk can be managed by software tools that contain fatigue and sleep behavior modeling, but optimization/validation of the model using the specific target population is required to ensure that the modeled predictions are accurate. The goal of the study was to validate the sleep behavior model settings for a fatigue modeling tool that is used within the RCAF, the Fatigue Avoidance Scheduling Tool, taking into account the organizational requirements for pre- and postflight routines, especially within the Air Mobility force. Materials and methods Four Royal Canadian Air Force Air Mobility Squadrons from Canadian Forces Base Trenton took part in this trial over a 3-month period (May 3 to August 21, 2016). All 22 missions of the trial included long-range transmeridian flights. All members of the participating aircrew wore wrist actigraphs to measure their sleep. We compared cognitive effectiveness modeling scenarios (preharmonization) based on the SAFTE-FAST sleep behavior model with its default settings against cognitive effectiveness modeling scenarios based on actigraphically-measured sleep. The measured sleep was then harmonized against the predicted sleep to optimize accuracy of the sleep behavior algorithm. During the harmonization process, the “Autosleep” prediction settings were optimized to match the actigraphically-measured sleep timings. Results Prior to the harmonization effort, the sleep behavior algorithm overpredicted the sleep obtained by CAF Aircrews. The most significant adjustment to the sleep behavior model was the increase in commute time to account for briefing, flight planning, debriefing, and postflight activities. Following harmonization, the sleep behavior model provided nearly perfect estimates of overall fatigue risk against missions modeled with actigraphically-measured sleep. For both measured and predicted sleep, most of the time in flight was in a low-fatigue, high-cognitive effectiveness state (90%–95% cognitive effectiveness). Conclusions Current Fatigue Risk Management Systems require accurate fatigue and sleep behavior modeling, which can only be achieved by studying specific target populations to determine their culture of work/rest routines, and optimizing sleep behavior model settings accordingly.

Sign in / Sign up

Export Citation Format

Share Document