Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
A Bidirectional Collaboration Framework for Bio-Model Development
Get PDFHigh-level graph data structures have gained favour in representing biologicalknowledge in a computationally executable form, but the information containedtherein must remain accessible to all users no matter their background. Bidirectionalgraph transformations may be used to synchronise and maintain the consistencyof these graph data structures as they evolve through the process of creatingand refining a bio-model knowledge base. We outline a bidirectional collaborationframework by which users with vastly differing backgrounds may contribute to thedevelopment and evolution of such a knowledge base, and examine a simple example to illustrate its merits. We also identify avenues for further research necessary to refine the framework. No prior biological knowledge is assumed
A Meta Model for Software Architecture Conformance and Quality Assessment
Get PDFSoftware architecture and design suffer from a lack of documented knowledge on how different architectural styles influence software quality. Existing software quality models do not allow engineers to evaluate whether a given software system adequately implements the basic principles of the chosen architectural style, and which architectural properties and best practices beyond these principles contribute to the system's quality. In this paper, I present a meta quality model for software architectures, which can be used not only as a knowledge-base to easily compare architectural styles based on their impact on software quality, but also to increase efficiency of architectural quality analysis by leveraging existing modeling concepts and tools. An experiment performing an architecture assessment using a quality model for the SOA architectural style not only showed that the approach is applicable in practice, but also indicated a reduction of manual effort compared to other architecture assessment approaches
A Formal Specification of the DNSSEC Model
Get PDFThe Domain Name System Security Extensions (DNSSEC) is a suite of specifications that provide origin authentication and integrity assurance services for DNS data. In particular, DNSSEC was designed to protect resolvers from forged DNS data, such as the one generated by DNS cache poisoning. This article presents a minimalistic specification of a DNSSEC model which provides the grounds needed to formally state and verify security properties concerning the chain of trust of the DNSSEC tree. The model, which has been formalized and verified using the Coq proof assistant, specifies an abstract formulation of the behavior of the protocol and the corresponding security-related events, where security goals, such as the prevention of cache poisoning attacks, can be given a formal treatment
Well-formed Model Co-evolution with Customizable Model Migration
Get PDFModel-driven engineering (MDE) is a software engineering discipline which focuses on models as the primary artifact of the software development process while programs are mainly generated by means of model-to-code transformations. In particular, modeling languages tailored to specific domains promise to increase the productivity and quality of software. Nevertheless due to e.g. evolving requirements, modeling languages evolve and existing models have to be migrated. Corresponding manual model migration is tedious and error-prone, therefore tools have been developed to (partly) automate this process. We follow the idea of considering such modeling language and model co-evolutions as related graph transformations ensuring a correct and unique typing of migrated models. In this paper, we present a general and formal construction of well-formed model migration schemes that are able to co-adapt any model of a given modeling language to a performed meta-model change. We show how appropriate model migration schemes can be constructed and discuss how they may be customized
Interactive Strategy-Based Validation of Behavioral Models
Get PDFWhen behavioral models are derived automatically based on observed stakeholder interactions, requirements engineers need to validate whether the stakeholders agree with the synthesized behavioral models. Allowing stakeholders to experience such models through simulation and animation allows them to comment on, amend to and correct these models. However, to ensure an efficient stakeholder validation, the simulation has to be guided instead of confronting the user with random situations over and over again. In this paper, we present a strategy-driven simulator capable of guiding the execution of behavioral models based on graph transformations. By analyzing either the overall structure of a partial state space (look ahead) or by performing an in-depth analysis of the states therein, the simulator is able to determine which transformations should be executed next to continue on the most promising path through the overall state space. The discussed implementation is illustrated with a case study
Process Scenarios in Open Source Software Certification
Get PDFCertification of Open Source Software (OSS) presents inherent trade-offsdue to the necessity of precisely identifying both a product and an independent certificationagent, and on the other of maintain the peculiar, valuable OSS characteristicof being available to an unlimited multiplicity of actors for trial, use and change.This is an intriguing challenge, usually solved by removing from the picture thecertifying agent and providing an intrinsic certification by means of rigorous, reapplicableproperty demonstrations, adopting Formal Methods (FM) in expressingand verifying the code. As such approach, yet quite valuable and good-promising,has some restrictions (such as the limited set of provable product qualities), we proposeto tackle the problem by analysing the various processes executed by differentOSS stakeholders, including the process of an independent Certification Body. Inthe paper some kinds of representative scenarios in which such processes interleaveare presented and discussed. The aim is to introduce a process-centered perspectivefor OSS that can stimulate research to further understand and mitigate the mentionedtrade-offs
Analysis of Hypergraph Transformation Systems in AGG based on M-Functors
Get PDFHypergraph transformation systems are examples of M-adhesive transformation systems based on M-adhesive categories. For typed attributed graph transformation systems, the tool environment AGG allows the modelling, the simu-lation and the analysis of graph transformations. A corresponding tool for analysis of hypergraph transformation systems does not exist up to now. The purpose of this paper is to establish a formal relationship between the corresponding M-adhesive transformation systems, which allows us the translation of hypergraph transformations into typed attributed graph transformations with equivalent behavior, and, vice versa, the creation of hypergraph transformations from typed attributed graph transformations. This formal relationship is based on the general theory of M-functors between different M-adhesive transformation systems. We construct a functor between the M-adhesive categories of hypergraphs and of typed attributed graphs, and show that our construction yields an M-functor with suitable properties. We then use existing results for M-functors to show that analysis results for hypergraph transformation systems can be obtained using AGG by analysis of the translated typed attributed graph transformation system. This is shown in general and for a concrete example
Monitor-Oriented Compensation Programming Through Compensating Automata
Get PDFCompensations have been used for decades in areas such as flow management systems, long-lived transactions and more recently in the service-oriented architecture. Since compensations enable the logical reversal of past actions, by their nature they crosscut other programming concerns. Thus, intertwining compensations with the rest of the system not only makes programs less well-structured, but also limits the expressivity of compensations due to the tight coupling with the system's behaviour. To separate compensation concerns from the normal system behaviour, we propose compensating automata, a graphical specification language dedicated to compensation programming. Compensating automata are subsequently employed in a monitor-oriented fashion to program compensations without cluttering the actual system implementation. This approach is shown applicable to a complex case study which existing compensation approaches have difficulty handling
