相关论文: Proceedings FM-09 Workshop on Formal Methods for A…

Software testing uses wide range of different tools to enhance the complicated process of defining quality of the system under test. Formal Concept Analysis (FCA) provides us with algorithms of deriving formal ontology from a set of objects…

The interest on autonomous systems is increasing both in industry and academia. Such systems must operate with limited human intervention in a changing environment and must be able to compensate for significant system failures without…

Formal methods were frequently shown to be effective and, perhaps because of that, practitioners are interested in using them more often. Still, these methods are far less applied than expected, particularly, in critical domains where they…

Aerial manipulation aims at combining the manoeuvrability of aerial vehicles with the manipulation capabilities of robotic arms. This, however, comes at the cost of the additional control complexity due to the coupling of the dynamics of…

The periodic inspection of vessels is a fundamental task to ensure their integrity and avoid maritime accidents. Currently, these inspections represent a high cost for the ship owner, in addition to the danger that this kind of hostile…

With advancements in technology, commercial aircraft formation flying is becoming increasingly feasible as an efficient and environmentally friendly flight method. However, gaps remain in practical implementation, particularly in collision…

One of the most challenging tasks in software specifications engineering for a multi-agent system is to ensure correctness. As these systems have high concurrency, often have dynamic environments, the formal specification and verification…

Integrating formal methods into industrial practice is a challenging task. Often, different kinds of expertise are required within the same development. On the one hand, there are domain engineers who have specific knowledge of the system…

Unmanned Aerial Vehicles (UAVs) are indispensable for infrastructure inspection, surveillance, and related tasks, yet they also introduce critical security challenges. This survey provides a wide-ranging examination of the anti-UAV domain,…

The current verification flow of complex systems uses different engines synergistically: virtual prototyping, formal verification, simulation, emulation and FPGA prototyping. However, none is able to verify a complete architecture.…

We propose a methodology for verifying security properties of network protocols at design level. It can be separated in two main parts: context and requirements analysis and informal verification; and formal representation and procedural…

Safety of medical devices and of their interoperation is an unresolved issue causing severe and sometimes deadly accidents for patients with shocking frequency. Formal methods, particularly in support of highly reusable and provably safe…

The integration of machine learning (ML) into cyber-physical systems (CPS) offers significant benefits, including enhanced efficiency, predictive capabilities, real-time responsiveness, and the enabling of autonomous operations. This…

The given paper considered a generalized model representation of the software system "Instrumental complex for ontological engineering purpose". Represented complete software system development process. Developed relevant formal models of…

It is our pleasure to present the papers of the sixth Working Formal Methods Symposium (FROM 2022) held at the "Al. I. Cuza" university of Iasi, Romania on September 19-20, 2022. FROM aims to bring together researchers and practitioners who…

Increased utilization of unmanned aerial vehicles (UAVs) in critical operations necessitates secure and reliable communication with Ground Control Stations (GCS). This paper introduces Aero-LLM, a framework integrating multiple Large…

Operators performing high-stakes, safety-critical tasks - such as air traffic controllers, surgeons, or mission control personnel - must maintain exceptional cognitive performance under variable and often stressful conditions. This paper…

The goal of this paper is to help mainstream programmers routinely use formal verification on their smart contracts by 1) proposing a new YAML-format for writing general-purpose formal specifications, 2) demonstrating how a formal…

Advances in machine learning (ML) open the way to innovating functions in the avionic domain, such as navigation/surveillance assistance (e.g. vision-based navigation, obstacle sensing, virtual sensing), speechto-text applications,…

This paper presents our ongoing work on spatio-temporal models for formal analysis and property-based testing. Our proposed framework aims at reducing the impedance mismatch between formal methods and practitioners. We introduce a set of…