Algebraic Semantics of OCL-constrained Metamodel Specifications

CS-09-001 Artur Boronat & Jose Meseguer.

In the definition of domain-specific languages a MOF metamodel is used to define the main types of its abstract syntax, and OCL invariants are used to add semantic constraints. The semantics of a metamodel definition can be given as a model type whose values are well-formed models. A model is said to conform to its metamodel when it is a value of the corresponding model type. However, when OCL invariants are involved, the concept of model conformance has not yet been formally defined in the MOF standard. In this work, the concept of OCL-constrained metamodel conformance is formally defined and used for defining style-preserving software architecture configurations. This concept is supported in MOMENT2, an algebraic framework for MOF metamodeling, where OCL constraints can be used for both static and dynamic analysis.

Available as: Adobe™ PDF (.pdf)

What is a Multi-Modeling Language?

CS-09-002 Artur Boronat , Alexander Knapp , Jose Meseguer & Martin Wirsing.

In large software projects often multiple modeling languages are used in order to cover the different domains and views of the application and the language skills of the developers appropriately. Such “multi-modeling” raises many methodological and semantical questions, ranging from semantic consistency of the models written in different sublanguages to the correctness of model transformations between the sublanguages. We provide a first formal basis for answering such questions by proposing semantically well-founded notions of a multimodeling language and of semantic correctness for model transformations. In our approach, a multi-modeling language consists of a set of sublanguages and correct model transformations between some of the sublanguages. The abstract syntax of the sublanguages is given by MOF meta-models. The semantics of a multi-modeling language is given by associating an institution, i.e., an appropriate logic, to each of its sublanguages. The correctness of model transformations is defined by semantic connections between the institutions.

Available as: Adobe™ PDF (.pdf)

A novel class of automata for languages on infinite alphabets Queries

CS-09-003 V.Ciancia & E.Tuosto.

Automata theory is fundamental in Computer Science; in formal language theory automata are used to characterise classes of languages of words over finite alphabets. In this paper we set the basis for a formal language theory inspired by nominal calculi (e.g. the p-calculus) and based on an automata framework amenable to deal with languages over infinite alphabets. Our aim is to develop a novel combination of formal languages over infinite alphabets and nominal calculi. More precisely, we focus on the basic definitions of recognisability of languages inspired by nominal calculi where new symbols may be “generated” to match symbols from an infinite alphabet. Our notion of recognisability is based on history-dependent (HDA). Noticeably, the most distinguished feature of HDA, namely locality of names, is pivotal in our approach.

Available as: Adobe™ PDF (.pdf)

Share this page:

Contact Us

Admissions Enquiries:
BSc: +44 (0) 116 252 5280
MSc: +44 (0) 116 252 2265
E: BSc  seadmissions@le.ac.uk
E: MSc  pgadmissions@le.ac.uk

Departmental Enquiries:
T: +44 (0) 116 252 2129/3887
F: +44 (0) 116 252 3604
E: csadmin@mcs.le.ac.uk

Dept of Informatics
University of Leicester
Leicester, LE1 7RH
United Kingdom


DisabledGo logo

The University of Leicester is committed to equal access to our facilities. DisabledGo has a detailed accessibility guide for the Informatics Building.