Standard

Automata-Based Software Engineering with Event-B. / Shelekhov, V. I.

In: Programming and Computer Software, Vol. 49, No. 5, 10.2023, p. 470-483.

Research output: Contribution to journal › Article › peer-review

Harvard

Shelekhov, VI 2023, 'Automata-Based Software Engineering with Event-B', Programming and Computer Software, vol. 49, no. 5, pp. 470-483. https://doi.org/10.1134/S0361768823050079

APA

Shelekhov, V. I. (2023). Automata-Based Software Engineering with Event-B. Programming and Computer Software, 49(5), 470-483. https://doi.org/10.1134/S0361768823050079

Vancouver

Shelekhov VI. Automata-Based Software Engineering with Event-B. Programming and Computer Software. 2023 Oct;49(5):470-483. doi: 10.1134/S0361768823050079

Author

Shelekhov, V. I. / Automata-Based Software Engineering with Event-B. In: Programming and Computer Software. 2023 ; Vol. 49, No. 5. pp. 470-483.

BibTeX

@article{4f3c6cd5dc0a4cdb877e1b66fb7269e2,
title = "Automata-Based Software Engineering with Event-B",
abstract = "A new automata-based programming language built by extending the Event-B specification language is proposed. When developing models in Event-B, it becomes possible to use automata-based methods in addition to the popular refinement method. The automata-based software engineering based on Event-B is demonstrated by the example of traffic control on a bridge from the Event-B system manual. A simpler solution with verification in the Rodin tool is proposed. The effectiveness of Event-B verification methods is confirmed by finding three nontrivial bugs in our solution.",
keywords = "Event-B, automata-based programming, deductive verification, functional programming, refinement, requirement, transformations of programs",
author = "Shelekhov, {V. I.}",
note = "Публикация для корректировки.",
year = "2023",
month = oct,
doi = "10.1134/S0361768823050079",
language = "English",
volume = "49",
pages = "470--483",
journal = "Programming and Computer Software",
issn = "0361-7688",
publisher = "Maik Nauka Publishing / Springer SBM",
number = "5",

}

RIS

TY - JOUR

T1 - Automata-Based Software Engineering with Event-B

AU - Shelekhov, V. I.

N1 - Публикация для корректировки.

PY - 2023/10

Y1 - 2023/10

N2 - A new automata-based programming language built by extending the Event-B specification language is proposed. When developing models in Event-B, it becomes possible to use automata-based methods in addition to the popular refinement method. The automata-based software engineering based on Event-B is demonstrated by the example of traffic control on a bridge from the Event-B system manual. A simpler solution with verification in the Rodin tool is proposed. The effectiveness of Event-B verification methods is confirmed by finding three nontrivial bugs in our solution.

AB - A new automata-based programming language built by extending the Event-B specification language is proposed. When developing models in Event-B, it becomes possible to use automata-based methods in addition to the popular refinement method. The automata-based software engineering based on Event-B is demonstrated by the example of traffic control on a bridge from the Event-B system manual. A simpler solution with verification in the Rodin tool is proposed. The effectiveness of Event-B verification methods is confirmed by finding three nontrivial bugs in our solution.

KW - Event-B

KW - automata-based programming

KW - deductive verification

KW - functional programming

KW - refinement

KW - requirement

KW - transformations of programs

UR - https://www.scopus.com/record/display.uri?eid=2-s2.0-85173617860&origin=inward&txGid=25e16a9a3eccbf2c75cff75c988480f6

UR - https://www.mendeley.com/catalogue/14c4005f-df6f-3e41-92b8-61ade9c161f7/

U2 - 10.1134/S0361768823050079

DO - 10.1134/S0361768823050079

M3 - Article

VL - 49

SP - 470

EP - 483

JO - Programming and Computer Software

JF - Programming and Computer Software

SN - 0361-7688

IS - 5

ER -

ID: 59548859