Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
A Note on Causalities in Reaction Systems
Get PDFReaction systems are a formal model of interactions between biochemical reactions. In this note we initiate an investigation of causalities in reaction systems which reflect the way that elements (entities) of a reaction system influence each other.
Keywords: natural computing; biochemical interactions; reaction systems; causal relationship
A MOP Based DSL for Testing Java Programs using OCL
Get PDFOCL is used to specify systems by defining pre and post-conditions for
class operations. Typically, the conditions refer to properties and operations that are
defined in a model. When the model is implemented, various implementation decisions
are made regarding properties and operations that cause the OCL conditions to
be inconsistent with the implementation. This paper defines a domain specific language
(DSL) for testing and shows how a meta-object-protocol for OCL can be used
to dynamically run tests written in the DSL against different Java implementations
of the same model
Component Certification as a Prerequisite forWidespread OSS Reuse
Get PDFOpen source software is the product of a community process that in a single project may employ different development techniques and volunteers with diverse skills, interests and hardware. Reuse of OSS software in systems that will have to guarantee certain product properties is still complicated. The main reason is the many different levels of trust that can be placed on the various OSS sources and the lack of information for the impact that a reused OSS component can have on the system properties. A prerequisite for promoting widespread reuse of OSS software is certification at the component level in an affordable cost. This work addresses the main technical issues behind OSS component certification by formal and semiformal techniques, as well as the incentives that raised the need for the OPEN-SME European funded project. OPEN-SME introduces an OSS software reuse service for SMEs, in order to address the problem that OSS evolves by volunteers that follow different development processes. We discuss the requirements relating to OSS software reuse based on the findings of a survey. Then we present the OPEN-SME tool-set and approach for OSS reuse and finally we show how the provision of verifiable certificates can provide assurance that an OSS component conforms to one or more anticipated requirements, necessary for reusing it in a system
On Judgements and Propositions
Get PDFThis article studies some of the relevant and historically inï¬uential conceptions of the notions of âjudgementâ and âpropositionâ and discusses the relationship of these notions in these conceptions. In some detail the conceptions of Aristoteles, Brentano and Twardowski, Frege, Martin-Löf and of epsilon-theory are presented. A comparison of these conceptions shows fundamental differences which, in a way, illuminate the differences found in the architectures and formal appearances of logics
Reaction Systems: a Formal Framework for Processes Based on Biochemical Interactions
Get PDFThis paper presents a formal framework for investigating processes driven
by interactions between biochemical reactions in living cells. These interactions are based on the mechanisms of facilitation and inhibition, which underlie the definition of reaction systems - the central construct of our framework. We discuss in this paper the basic setup for reaction systems, and its motivation. We also present an important extension of reaction systems as well as some research topics and results
Expressiveness of graph conditions with variables
Get PDFGraph conditions are very important for graph transformation systems and graph programs in a large variety of application areas. Nevertheless, non-local graph properties like ``there exists a path'', ``the graph is connected'', and ``the graph is cycle-free'' are not expressible by finite graph conditions. In this paper, we generalize the notion of finite graph conditions, expressively equivalent to first-order formulas on graphs, to finite \HR^+ graph conditions, i.e., finite graph conditions with variables where the variables are place-holders for graphs generated by a hyperedge replacement system. We show that graphs with variables and replacement morphisms form a weak adhesive HLR category. We investigate the expressive power of \HR^+ graph conditions and show that finite \HR^+ graph conditions are more expressive than monadic second-order graph formulas
Checking Graph-Transformation Systems for Confluence
Get PDFIn general, it is undecidable whether a terminating graph-transformation
system is confluent or not. We introduce the class of coverable hypergraph-transformation systems and show that confluence is decidable for coverable systems that are terminating. Intuitively, a system is coverable if its typing allows to extend each critical pair with a non-deletable context that uniquely identifies the persistent nodes of the pair. The class of coverable systems includes all hypergraph-transformation systems in which hyperedges can connect arbitrary sequences of nodes, and all graph-transformation systems with a sufficient number of unused edge labels
Towards the Verification of Pervasive Systems
Get PDFPervasive systems, that is roughly speaking systems that can interact with their environment, are increasingly common. In such systems, there are many dimensions to assess: security and reliability, safety and liveness, real-time response, etc. So far modelling and formalizing attempts have been very piecemeal approaches. This paper describes our analysis of a pervasive case study (MATCH, a homecare application) and our proposal for formal (particularly verification) approaches. Our goal is to see to what extent current state of the art formal methods are capable of coping with the verification demand introduced by pervasive systems, and to point out their limitations
MySQL4OCL: A Stored Procedure-Based MySQL Code Generator for OCL
Get PDFIn this paper we introduce a MySQL code generator for a significant subset of OCL expressions which is based on the use of stored procedures for mapping OCL iterators. Our code generator is defined recursively over the structure of OCL expressions. We discuss the class of OCL expressions covered by our definition (which includes, possibly nested, iterator expressions) as well as some extensions needed to cover the full OCL language. We also discuss the efficiency of the MySQL code produced by our code generator, and compare it with previous known results on evaluating OCL expressions on medium-large scenarios. We have implemented our code generator in the MySQL4OCL tool