相关论文: Time4sys2imi: A tool to formalize real-time system…

Within academia and industry, there has been a need for expansive simulation frameworks that include model-based simulation of sensors, mobile vehicles, and the environment around them. To this end, the modular, real-time, and open-source…

This volume contains the proceedings of MARS 2022, the fifth workshop on Models for Formal Analysis of Real Systems, held as part of ETAPS 2022, the European Joint Conferences on Theory and Practice of Software. The MARS workshops bring…

Multivariate time-series forecasting is vital in various domains, e.g., economic planning and weather prediction. Deep train-from-scratch models have exhibited effective performance yet require large amounts of data, which limits real-world…

As the development of autonomous vehicles progresses, efficient safety assurance methods become increasingly necessary. Safety assurance methods such as monitoring and scenario-based testing call for formalisation of driving scenarios. In…

We present a simple and concise semantics for temporal planning. Our semantics are developed and formalised in the logic of the interactive theorem prover Isabelle/HOL. We derive from those semantics a validation algorithm for temporal…

Parametric analysis is a powerful tool for designing modern embedded systems, because it permits to explore the space of design parameters, and to check the robustness of the system with respect to variations of some uncontrollable…

Simulation is a prospective method for generating diverse and realistic traffic scenarios to aid in the development of driving decision-making systems. However, existing simulators often fall short in diverse scenarios or interactive…

The Robot Operating System (ROS) is one of the most popular middleware for developing robot applications, but it is subject to major shortcomings when applied to real-time robotic systems in safety-critical environments. For this reason,…

We propose TRACIE, a novel temporal reasoning dataset that evaluates the degree to which systems understand implicit events -- events that are not mentioned explicitly in natural language text but can be inferred from it. This introduces a…

Most research on formal system design has focused on optimizing various measures of efficiency. However, insufficient attention has been given to the design of systems optimizing resilience, the ability of systems to adapt to unexpected…

This paper introduces time window temporal logic (TWTL), a rich expressivity language for describing various time bounded specifications. In particular, the syntax and semantics of TWTL enable the compact representation of serial tasks,…

System identification involves constructing mathematical models of dynamic systems using input-output data, enabling analysis and prediction of system behaviour in both time and frequency domains. This approach can model the entire system…

This EPTCS volume contains the joint proceedings for the fourth international workshop on Formal Methods for Autonomous Systems (FMAS 2022) and the fourth international workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE…

Timed model checking has been extensively researched in recent years. Many new formalisms with time extensions and tools based on them have been presented. On the other hand, Explicit-Time Description Methods aim to verify real-time systems…

We revisit the problem of real-time verification with dense dynamics using timeout and calendar based models and simplify this to a finite state verification problem. To overcome the complexity of verification of real-time systems with…

We formalize synthesis of shared control protocols with correctness guarantees for temporal logic specifications. More specifically, we introduce a modeling formalism in which both a human and an autonomy protocol can issue commands to a…

This volume contains the proceedings of MARS 2024, the sixth workshop on Models for Formal Analysis of Real Systems, held as part of ETAPS 2024, the European Joint Conferences on Theory and Practice of Software. The MARS workshops bring…

Model checking for real-timed systems is a rich and diverse topic. Among the different logics considered, Metric Interval Temporal Logic (MITL) is a powerful and commonly used logic, which can succinctly encode many interesting timed…

Interrupt Timed Automata (ITA) is an expressive timed model, introduced to take into account interruptions, according to levels. Due to this feature, this formalism is incomparable with Timed Automata. However several decidability results…

Formal explainable artificial intelligence (XAI) offers unique theoretical guarantees of rigor when compared to other non-formal methods of explainability. However, little attention has been given to the validation of practical…