This paper presents an abstract machine that can be easily used to teach intermediate and source code optimization, fundamental issues in a course on compiler construction techniques, bringing together theory and practice of computer science in a simple way.
Designing and verifying safety-critical systems requires giving equal importance to non-functional and functional requirements from the start, especially those related to time. Since no single method can address all system aspects, a combination of formal methods is needed for accurate modeling and analysis. This paper proposes an integration of the CCSL (Clock constraints Specification language) and TASTD specification languages for the modular modeling of timing requirements. CCSL allows for the modular expression of timing constraints, whereas TASTD 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 a TASTD specification, which can use the CSP [14] operators of TASTD to compose the CCSL constraints with other specification elements, like operating modes of a system. The CCSL part of the specification can be verified using CCSL tools. The global specification can be simulated using TASTD tools. The approach is demonstrated on a temperature control system which has been previously modeled using UML MARTE and CCSL, but for which no formal combination was available.
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 for the 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 accurate semantic inspection 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.
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-based Epistemic Logic of 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.
Workflows coordinate tasks across departments or organisations, where correct execution depends not only on control dependencies but also on the availability of shared resources. This paper presents ReAct, a resource-aware active object language for workflow modelling. In ReAct, method declarations serve as contracts: they specify alternative resource profiles in their signatures, giving methods multiple execution options when resources are limited. Methods can be invoked only once their dependency conditions are satisfied; at activation, a feasible resource profile is then selected and allocated. We encode the language in Maude and show how workflows can be executed, simulated, and verified against their declared dependencies and resource requirements.
