Abstract By bridging the semantic gap, domain-specific language (DSLs) serve an important role in the conquest to allow domain experts to model their systems themselves. In this publication we present a case study of the development of the Continuous REactive SysTems language (CREST), a DSL for hybrid systems modeling. The language focuses on the representation of continuous resource flows such as water, electricity, light or heat. Our methodology follows a very pragmatic approach, combining the syntactic and semantic principles of well-known modeling means such as hybrid automata, data-flow languages and architecture description languages into a coherent language. The borrowed aspects have been carefully combined and formalised in a well-defined operational semantics. The DSL provides two concrete syntaxes: CREST diagrams, a graphical language that is easily understandable and serves as a model basis, and , an internal DSL implementation that supports rapid prototyping—both are geared towards usability and clarity. We present the DSL’s semantics, which thoroughly connect the various language concerns into an executable formalism that enables sound simulation and formal verification in , and discuss the lessons learned throughout the project.

Swift is a modern general-purpose programming language, designed to be a replacement for C-based languages. Although primarily directed at development of applications for Apple's operating systems, Swift's adoption has been growing steadily in other domains, ranging from server-side services to machine learning. This success can be partly attributed to a rich type system that enables the design of safe, fast, and expressive programming interfaces. Unfortunately, this richness comes at the cost of complexity, setting a high entry barrier to exploit Swift's full potential. Furthermore, existing documentation typically only relies on examples, leaving new users with little help to build a deeper understanding of the underlying rules and mechanisms.

Representing and reasoning on contexts is an open problem in the semantic web. Despite the fact that context representation has for a long time been treated locally by semantic web practitioners, a recognized and widely accepted consensus regarding the way of encoding and particularly reasoning on contextual knowledge has not yet been reached by far. In this paper, we present OWL^C : a contextual two-dimensional web ontology language. Using the first dimension, we can reason on contexts-dependent classes, properties, and axioms and using the second dimension, we can reason on knowledge about contexts which we consider formal objects, as proposed by McCarthy [McCarthy, 1987]. We demonstrate the modeling strength and reasoning capabilities of OWL^C with a practical scenario from the digital humanity domain. We chose the Ferdinand de Saussure [Joseph, 2012] use case in virtue of its inherent contextual nature, as well as its notable complexity which allows us to highlight many issues connected with contextual knowledge representation and reasoning.

Aliasing is a vital concept of programming, but it comes with a plethora of challenging issues, such as the problems related to race safety. This has motivated years of research, and promising solutions such as ownership or linear types have found their way into modern programming languages. Unfortunately, most current approaches are restrictive. In particular, they often enforce a single-writer constraint, which prohibits the creation of mutable self-referential structures. While this constraint is often indispensable in the context of preemptive multithreading, it can be worked around in the case of single threaded programs. With the recent resurgence of cooperative multitasking, where processes voluntarily share control over a single execution thread, this appears to be interesting trade-off. In this paper, we propose a type system that relaxes the usual single-writer constraint for single threaded programs, without sacrificing race safety properties. We present it in the form of a simple reference-based language, for which we provide a formal semantics, as well as an interpreter.

Modularity is a mandatory principle to apply Petri nets to real world-sized systems. Modular extensions of Petri nets allow to create complex models by combining smaller entities. They facilitate the modeling and verification of large systems by applying a divide and conquer approach and promoting reuse. Modularity includes a wide range of notions such as encapsulation, hierarchy and instantiation. Over the years, Petri nets have been extended to include these mechanisms in many different ways. The heterogeneity of such extensions and their definitions makes it difficult to reason about their common features at a general level. We propose in this article an approach to standardize the semantics of modular Petri nets formalisms, with the objective of gathering even the most complex modular features from the literature. This is achieved with a new Petri nets formalism, called the LLAMAS Language for Advanced Modular Algebraic Nets (LLAMAS). We focus principally on the composition mechanism of LLAMAS, while introducing the rest of the language with an example. The composition mechanism is introduced both informally and with formal definitions. Our approach has two positive outcomes. First, the definition of new formalisms is facilitated, by providing common ground for the definition of their semantics. Second, it is possible to reason at a general level on the most advanced verification techniques, such as the recent advances in the domain of decision diagrams.

Although model checking is heavily used in the hardware domain, it did not take off in software engineering yet. One of the possible reasons is that software models are very complex. They integrate many dimensions such as data types and concurrency,

Designing a DSML implies binding the syntactical concepts of the problem domain with the semantics of a solution domain. Previous work presented a formal framework for language composition where language syntactical patterns (expressed by metamodels) along with their semantics (expressed by transformation models) are combined as small reusable building blocks in a constructive manner, in order to achieve the desired expressiveness for DSMLs. This article refines the framework, as well as showing its application through a case study led in collaboration with CERN (European Organization for Nuclear Research).

A work-in-progress domain-specific language and methodology for modeling complex control systems GUIs is presented. MDA techniques are applied for language design and verification, simulation and prototyping.

In this paper, we present the Concurrent Object-Oriented Petri Nets (CO-OPN/2) formalism devised to support the specification of large distributed systems. Our approach is based on two underlying formalisms: order-sorted algebra and algebraic Petri nets. With respect to the lack of structuring capabilities of Petri nets, CO-OPN/2 has adopted the object-oriented paradigm. In this hybrid approach (model- and property-oriented), classes of objects are described by means of algebraic Petri nets, while data structures are expressed by order-sorted algebraic specifications. An original feature is the sophisticated synchronization mechanism. This mechanism allows to involve many partners in a synchronization and to describe the synchronization policy. A typical example of distributed systems, namely the Transit Node, is used throughout this paper to introduce our formalism and the concrete specification language associated with it. By successive refinements of the components of the example, we present, informally, most of the notions of CO-OPN/2. We also give some insights about the coordination layer, Context and Objects Interface Language (COIL), which is built on top of CO-OPN/2. This coordination layer is used for the description of the concrete distributed architecture of the system. Together, CO-OPN/2 and COIL provide a complete formal framework for the specification of distributed systems.

The techniques and the tools developed to produce prototypes from CO-OPN (concurrent object-oriented Petri net) specifications are described. CO-OPN is a specification language for the description of concurrent aspects and data-structure aspects of computer programs in an abstract way. The concurrent part of the formalism is described with Petri nets, while the data aspects are described with algebraic abstract data types. In CO-OPN, this association is structured by the object notion. For prototyping such a formalism, a fully operational semantics is required. The semantics is given for the simulation tools that have been developed. An editor and an environment for executing CO-OPN specifications have been developed. The specifications are prototyped using a translation of the specifications into Prolog.>