Automated formalization of structured natural language requirements
D Giannakopoulou, T Pressburger, A Mavridou… - Information and …, 2021 - Elsevier
The use of structured natural languages to capture requirements provides a reasonable
trade-off between ambiguous natural language and unintuitive formal notations. There are …
trade-off between ambiguous natural language and unintuitive formal notations. There are …
Integrating formal verification and assurance: an inspection rover case study
The complexity and flexibility of autonomous robotic systems necessitates a range of distinct
verification tools. This presents new challenges not only for design verification but also for …
verification tools. This presents new challenges not only for design verification but also for …
Formal requirements modeling for cyber-physical systems engineering: An integrated solution based on FORM-L and Modelica
The increasing complexity of cyber-physical systems (CPSs) makes their design,
development and operation extremely challenging. Due to the nature of CPS that involves …
development and operation extremely challenging. Due to the nature of CPS that involves …
Automated translation of natural language requirements to runtime monitors
Runtime verification (RV) enables monitoring systems at runtime, to detect property
violations early and limit their potential consequences. This paper presents an end-to-end …
violations early and limit their potential consequences. This paper presents an end-to-end …
Capture, analyze, diagnose: realizability checking of requirements in FRET
A Katis, A Mavridou, D Giannakopoulou… - … on Computer Aided …, 2022 - Springer
Requirements formalization has become increasingly popular in industrial settings as an
effort to disambiguate designs and optimize development time and costs for critical system …
effort to disambiguate designs and optimize development time and costs for critical system …
[HTML][HTML] Towards a method to quantitatively measure toolchain interoperability in the engineering lifecycle: A case study of digital hardware design
JM Alvarez-Rodríguez, R Mendieta, E Cibrián… - Computer Standards & …, 2023 - Elsevier
The engineering lifecycle of cyber-physical systems is becoming more challenging than
ever. Multiple engineering disciplines must be orchestrated to produce both a virtual and …
ever. Multiple engineering disciplines must be orchestrated to produce both a virtual and …
FRETting about requirements: formalised requirements for an aircraft engine controller
M Farrell, M Luckcuck, O Sheridan… - … Working Conference on …, 2022 - Springer
Abstract [Context & motivation] Eliciting requirements that are detailed and logical enough to
be amenable to formal verification is a difficult task. Multiple tools exist for requirements …
be amenable to formal verification is a difficult task. Multiple tools exist for requirements …
From partial to global assume-guarantee contracts: compositional realizability analysis in FRET
A Mavridou, A Katis, D Giannakopoulou, D Kooi… - Formal Methods: 24th …, 2021 - Springer
Realizability checking refers to the formal procedure that aims to determine whether an
implementation exists, always complying to a set of requirements, regardless of the stimuli …
implementation exists, always complying to a set of requirements, regardless of the stimuli …
Fretting and formal modelling: a mechanical lung ventilator
In this paper, we use NASA's Formal Requirements Elicitation Tool (FRET) and the Event-B
formal method to model and verify the requirements for the ABZ 2024 case study, the …
formal method to model and verify the requirements for the ABZ 2024 case study, the …
Authoring, analyzing, and monitoring requirements for a lift-plus-cruise aircraft
Abstract [Context & Motivation] Requirements specification and analysis is widely applied to
ensure the correctness of industrial systems in safety critical domains. Requirements are …
ensure the correctness of industrial systems in safety critical domains. Requirements are …