Research meeting March 6, 2012

Lloyd Rutledge: From ontology to wiki - Automatic generation of data input systems from Semantic Web ontologies

The Semantic Web's Linked Open Data Cloud now contains billions of data objects and is becoming an increasingly important source of data. Wikipedia, various national governments and large digital libraries are some of the many different types of contributors to the Linked Open Data Cloud. To put one's one data (for example, publications of a faculty) on the Linked Open Data Cloud effectively, it is important to use a data model, or ontology, that also other contributors with the same type of data also use. In this way, the data from different parties link together as part of the same knowledge domain. Ontologies on the Semantic Web technologies determined to be standardized is made available.

OWL Wiki Forms is a system that processes Semantic Web ontologies to set up a wiki that allows users to enter data that fit in these ontologies. The input data then becomes accessible via the wiki on the Linked Open Data Cloud. OWL Wiki Forms applies concepts from Model-Driven Development to make an extendible default data query, browse and import system based on a given data model. The result is the quick set up of a distributed and accessible interface for the collaborative input and maintenance of data on the Linked Open Data Cloud.

Ella Roubtsova: Motivation modelling

Services  are goal-oriented software systems and need to influence or motivate,  favour or dis-favour particular behaviour of their communication parties: humans and other services. This talk  investigates modelling of motivation for human-service interaction. It shows why motivation needs a separate model different from the service process model, how to specify motivation and compose the model with the service process model. Depending on the goal, each  service may have different motivation models and different human-computer interface. We provide  an example of a service model with different motivation models  that stimulate different behaviour of humans communicating with the service. The paper shows that motivation modelling  is yet another way of service reuse in different systems.

Debbie Tarenskeen: Non-functional requirements in software architectures with Ampersand as an Architectural Description Language

Can we relate software architectures to rules and evaluate the architectural design?

The basic problem of this research is how to relate non-functional requirements to software architectures (for instance: maintainability, efficiency) in a model. Requirements consists of functional requirements stated as needs of the stakeholders of what the system needs to accomplish (business needs) and non-functional requirements concerning the way the system should operate. The latter can be seen as qualitative system attributes for operating and managing the software. Characteristic of quality attributes is that system designs that contribute to one (or more) of the quality attributes have a disadvantage on one or more of the other quality attributes (trade off).

Ampersand is chosen as a software architecture description language for modeling software architectures and accompanying rules for achieving quality attributes for the following reasons:

• The main goal is to check if software architectures comply to rules of patterns that contribute to nonfunctional requirements
• Ampersand is based on rules and relation algebra, so it is suited to support formalization/modeling of software and patterns.

Freek Verbeek: Formal verification of on-chip communication fabrics with a focus on deadlock freedom

In the multicore era, on-chip communication fabrics play a vital role in the performance, power consumption and scalability of chips. The traditional bus is replaced with complex Network-on-Chip structures. This introduces many issues such as deadlocks, livelocks, and starvation. We apply formal verification to prove correctness of on-chip communication fabrics. The GeNoC methodology is presented, where abstract mathematical theorems are formally proven once-and-for-all on a generic Network-on-Chip model, so that proving correctness of a chip is reduced to the discharging of some easy proof obligations. GeNoC requires the chip to be modelled in the logic of the theorem prover ACL2. An objective is to increase applicability and usability of GeNoC by allowing modelling of chips in a designer-friendly language introduced by Intel, called xMAS. We present xMAS and an algorithm that automatically decides deadlock freedom of networks defined in this language.

Bernard van Gastel: Towards memory models in network-on-chips using message dependencies

Great progress has been made in formal verification of correct execution of software under a specific memory model. However, little work has been done in formal verification of hardware implementations to verify that they implement a memory model. To work with memory models we first have to incorporate message dependencies, message duplication, message merging and the concept of memory units in our formal GeNoC model. In this presentation I will introduce to you message {dependencies, duplication, merging} and of course memory models.

Bas Joosten: ELVeN: Effective Layered Verification of Networks on chips

Complex Networks-on-Chips (NoC) will replace the traditional bus architecture to efficiently support communications between the cores. It is urgent to provide the Electronic Design Automation community with methods for the formal validation of high-level and parametric specifications of NoCs architectures and the verification of their correct implementation at the Register Transfer Level (RTL).

ELVeN focuses on ensuring functional correctness of parametric designs and aims at a verification methodology spanning the full trajectory from high-level specifications down to implementations at the RTL. ELVeN will integrate a generic model of NoC architectures, a theory of refinements, and the combination of interactive and automatic verification techniques. This forms a scalable environment for the formal verification of the correct implementation of NoC designs. In this talk, we present some techniques that we hope to be valuable for achieving the goal of ELVeN, and by that the long-term goal of creating a science of NoC designs.