ABSTRACT. This paper investigates the enforcement of state-based security properties in process systems through supervisory control. We introduce a supervisor that operates under the assumption of incomplete system knowledge, mirroring the challenges faced in real-world deployments where both the supervisor and potential adversaries possess limited information. The proposed supervisor rectifies insecure process behaviors by strategically restricting actions or injecting timed events. Our study focuses on analyzing the necessary and sufficient conditions for the existence of such a supervisor capable of guaranteeing process security despite the knowledge limitations.

ABSTRACT. The formal design and verification of safety-critical systems requires capturing non-functional requirements with the same impor- tance as functional requirements, right from the beginning. Time plays a special role as many non-functional requirements directly depend upon it. Several specification languages have been proposed to deal with vari- ous aspects of a critical system, but no single method can simultaneously take into account all the different facets of a system to be developed or analyzed. Hence, there is a need to use a combination of formal methods to model as faithfully as possible all aspects of a system. This paper proposes an integration of the CCSL and ASTD specification languages for the modular modeling of timing requirements. CCSL allows for the modular expression of timing constraints, whereas ASTD allows for the combination of state machines using CSP process algebra operators, to foster the construction of a system specification using the composition of small components specification. We propose rules to translate a CCSL specification into an ASTD specification, which can use the CSP opera- tors of ASTD to compose the CCSL constraints with other specification elements, like operating modes of a system. The CCSL part of the speci- fication can be verified using CCSL tools. The global specification can be simulated using ASTD tools. The approach is demonstrated on a tem- perature control system which has been previously modeled using UML MARTE and CCSL, but for which no formal combination was available.

ABSTRACT. De Zolt's postulate is a more mathematically precise restatement of Euclid's geometric principle of ``the whole is greater than the part''~\cite[Book I, Common Notion 5]{heath56euclid}. While the three-dimensional version of De Zolt's postulate is not consistent with \zfc{} due to the Banach-Tarski paradox and related theorems, it is consistent with a proof-theoretically weaker theory. In this paper, we provide an implementation of such a weak type theory and a formal proof of De Zolt's postulate in three dimensions in this theory.

ABSTRACT. The B-Method is a formal specification and development methodology that ensures system correctness with a design-by-contract approach. However, translating these high-level specifications into C code introduces challenges, particularly in verifying that the generated code respects the specified properties. To address this, we propose a systematic translation process from the B-Method to ACSL, which enables the formal verification of C code using Frama-C, a static analysis tool. The proposed method provides a set of ACSL specifications that correspond to B-Method abstractions, allowing for deductive verification of C code to ensure compliance with safety and correctness requirements. A case study demonstrates the practical application of this translation strategy, showing its effectiveness in verifying a simple runner-counting system.

ABSTRACT. Model-Based Systems Engineering (MBSE) has made substantial progress in managing system complexity, yet it still lacks principled support for understanding system behavior during early design. SysML v2 introduces a richer semantics for modeling behavior, but its utility remains limited by a lack of executable semantics, weak interoperability, and the absence of native support for formal verification and design-space exploration. We argue that a paradigm shift is needed, one in which behavioral models become first-class, executable artifacts, navigable within a dynamic design multiverse.

This position paper presents the vision behind Living SysML v2 Blueprint, a next-generation SysML v2 virtual machine that unifies dynamic execution, multiverse exploration, and native formal verification. Central to this vision is the Transparent Execution, Observation, and Control (TEOC) API, enabling semantically faithful introspection and tool interoperability without model transformation. By tolerating incomplete models and exposing structured execution traces, the LivingBlueprint VM empowers system engineers, verification experts, and business strategists to engage with design decisions iteratively, rigorously, and early.

This architecture redefines the semantics–verification–execution triad at the heart of MBSE, offering new foundations for explainability, trust, and AI-augmented design. This paper outlines the theoretical pillars, practical challenges, and community-wide opportunities of this approach and invites collaborative efforts toward a new class of MBSE platforms centered around behavioral fidelity and multiverse awareness.

ABSTRACT. Multi-agent systems operating in real-world environments must reason about knowledge and information under uncertainty, with varying degrees of trust and incomplete evidence. While Dynamic Epistemic Logic (DEL) provides a robust framework for modeling knowledge change, its classical binary foundation limits its applicability to scenarios involving gradations of truth and knowledge. The Bilattice Logic of Epistemic Actions and Knowledge (BEAK) addresses this limitation by grounding DEL in bilattice structures, but restricts its semantics to the four-valued bilattice FOUR, limiting expressiveness for complex applications. This paper introduces GEAK (Generalized Bilattice Logic of Epistemic Actions and Knowledge), a generalization of BEAK that operates over arbitrary logical bilattices. GEAK preserves the elegant product update mechanism of DEL while extending it to handle multi-valued accessibility relations with custom truth-value structures tailored to specific domains. We present the formal syntax and semantics of GEAK, demonstrate its theoretical properties, and provide a model checker for bilattice-based dynamic epistemic logic. Our contributions are validated through a case study using Ginsberg's seven-valued default logic for multi-agent route planning, where autonomous vehicles coordinate under uncertainty with default assumptions about road conditions. Preliminary results suggest that GEAK offers greater expressiveness than classical approaches while maintaining computational tractability, enabling more realistic modeling and verification of multi-agent systems with sophisticated reasoning patterns involving definite and default information.