Development of concurrent systems in B AMN

This paper outlines an approach to extending B AMN to support concurrent specification, using a combination of linear temporal logic and Ada style task definitions. The extension is applied to the "production cell" case study.

• Publication year

  1996

• Venue

  Unknown venue

• Publication date

  1996-07-03

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.14236/EWIC/RW1996.8
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• The extension is applied to the production cell case study as a concrete example.

  Confidence 0.90

  박진우 (dztg5apj7m) extractionAK (4715169a40) reviewKiller Whale (322360f1c1) reviewB (s683577b42) review
• B AMN is extended to support concurrent specification by combining linear temporal logic with Ada style task definitions.

  Confidence 0.95

  박진우 (dztg5apj7m) extractionAK (4715169a40) reviewKiller Whale (322360f1c1) reviewB (s683577b42) review

• ada style task definitions

  language construct, concurrency construct

  Concurrency-oriented task constructs modeled after the task abstraction used in Ada.

  Aliases: Ada tasks, task definitions

  박진우 (dztg5apj7m) extractionAK (4715169a40) reviewKiller Whale (322360f1c1) reviewB (s683577b42) review
• b amn

  formalism

  The formal specification framework used as the base system that is being extended in the paper.

  Aliases: B-AMN, B AMN formalism

  박진우 (dztg5apj7m) extractionAK (4715169a40) reviewKiller Whale (322360f1c1) reviewB (s683577b42) review
• concurrent specification

  specification approach

  A specification style for describing system behavior with multiple activities that can proceed in parallel or interact over time.

  Aliases: concurrent system specification, specification of concurrency

  박진우 (dztg5apj7m) extractionAK (4715169a40) reviewKiller Whale (322360f1c1) reviewB (s683577b42) review
• linear temporal logic

  logic, temporal logic

  A temporal logic used to express properties of executions over time.

  Aliases: LTL

  박진우 (dztg5apj7m) extractionAK (4715169a40) reviewKiller Whale (322360f1c1) reviewB (s683577b42) review
• production cell case study

  case study

  The production-cell example used in the paper to demonstrate the proposed extension.

  Aliases: production cell, cell case study

  박진우 (dztg5apj7m) extractionAK (4715169a40) reviewKiller Whale (322360f1c1) reviewB (s683577b42) review

• Stepwise Refinement of Communicating Systems

  1996cited by this paper
• Interconnecting formalisms: supporting modularity, reuse and incrementality

  1995cited by this paper
• Reactive System Specification and Refinement

  1995cited by this paper
• Specifying Properties of Basic LOTOS Processes Using Temporal Logic

  1995cited by this paper
• Formal object-oriented development

  1995cited by this paper
• Safety-critical systems, formal methods and standards

  1993cited by this paper
• Role of VDM(++) in the Development of a Real-Time Tracking and Tracing System

  1993cited by this paper
• Formal specification in the development of industrial applications: Subway speed control system

  1992cited by this paper
• VITAL CODED PROCESSOR AND SAFETY RELATED SOFTWARE DESIGN

  1992cited by this paper
• The Raise Specification Language

  1992cited by this paper
• The Z notation: a reference manual

  1992cited by this paper
• The ESTEREL language

  1991cited by this paper

• que s emantique temporelle pour B

  2007cites this paper
• Contribution à l'intégration de temporalité au formalisme B : Utilisation du calcul des durées en tant que sémantique temporelle pour B

  2006cites this paper
• Program Development by Refinement

  1999cites this paper
• An Approach to the Design of Distributed Systems with B AMN

  1997cites this paper
• Using B to Design and Verify Controllers forChemical

  1996cites this paper
• Distributed System Development in B

  1996cites this paper