Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Adaptive Task Automata with Earliest-Deadline-First Scheduling
Get PDFAdjusting to resource changes, dynamic environmental conditions, or new usage modes are some of the reasons why real-time embedded systems need to be adaptive. This requires a rigorous framework for designing such systems, to ensure that the adaptivity does not result in invalidating the system’s real-time constraints. To address this need, we have recently introduced adaptive task automata, a framework for modeling, verification, and schedulability analysis in adaptive, hard real-time embedded systems, assuming a fixed-priority scheduler. In this work, we extend the adaptive task automata framework to incorporate the earliest-deadline-first scheduling policy, as well as enable implementation of any other dynamic scheduling policy. To prove the decidability of our model, and at the same time maintain a manageable degree of conciseness, we show an encoding of our model as a network of timed automata with clock updates. To support this, we also show that reachability in our class of timed automata with updates is decidable. Our contribution helps to streamline the process of designing safety critical adaptive embedded systems
Special Issue of PPAP 2013: Preface
No full textOn the 5th of March, 2013, the first workshop on Patterns Promotion and Anti-patterns Prevention (PPAP 2013) took place in Genova, Italy. PPAP 2013 was co-located with the 17th European Conference on Software Maintenance and Reengineering (CSMR'2013), the premier European conference on the theory and practice of maintenance, reengineering and evolution of software systems. With the aim of promoting the application of patterns and prevent the spread of anti-patterns, the first objective of PPAP is to build a bridge between the different families of patterns and anti-patterns in software engineering
Software Language Engineering by Intentional Rewriting
Get PDFGrammars in a broad sense (specifications of structural commitments) are complex artefacts that define software languages. Assessing and improving their quality in an automated, non-idiosyncratic manner is an unsolved problem which we face in an especially acute form in the case of mass maintenance of hundreds of heterogeneous grammars (parser specs, ADTs, metamodels, XML schemata, etc) in the Grammar Zoo. In an attempt to apply software language engineering methods to solve a software language engineering problem, we design a language for grammar mutations capable of applying uniform intentional transformations in the scope of a big grammar or a corpus of grammars. In this paper, we describe a disciplined process of engineering such a language by systematic reuse of semantic components of another existing software language. The constructs of the reference language are analysed and classified by their intent, each category of constructs is then subjected to rewriting. This process results in a set of constructs that form the new language
Comparing communication and development networks for predicting file change proneness: An exploratory study considering process and social metrics
Get PDFPrevious studies have shown that social factors of software engineering influence software quality. Communication and development networks represent the interactions among software developers. We explored the statistical relationships between file change proneness and a set metrics extracted from the issue tracker and version control system data to find the relative importance of each metric inunderstanding the evolution of file changes in the Rails project. Using hierarchical analysis, we found that code churn, number of past changes, and number of developers explain the evolution of changes in the Rails project better than Social NetworkAnalysis (SNA) metrics. Considering the relative importance of each predictor, wegot the same results. We also conducted a factor analysis and found that social metrics contribute to explain a group of files different from those explained by process metrics
Solving the N-Queens Problem with GROOVE - Towards a Compendium of Best Practices
Get PDFWe present a detailed solution to the N-queens puzzle using GROOVE, a graph transformation tool especially designed for state space exploration and analysis. While GROOVE has been freely available for more than a decade and has attracted a reasonable number of users, it is safe to say that only a few of these users fully exploit the tool features. To improve this situation, using the N-queens puzzle as a case study, in this paper we provide an in-depth discussion about problem solving with GROOVE, at the same time highlighting some of the tool's more advanced features. This leads to a list of best-practice guidelines, which we believe to be useful to new and expert users alike
Reachability and Reward Checking for Stochastic Timed Automata
Get PDFStochastic timed automata are an expressive formal model for hard and soft real-time systems. They support choices and delays that can be deterministic, nondeterministic or stochastic. Stochastic choices and delays can be based on arbitrary discrete and continuous distributions. In this paper, we present an analysis approach for stochastic timed automata based on abstraction and probabilistic model checking. It delivers upper/lower bounds on maximum/minimum reachability probabilities and expected cumulative reward values. Based on theory originally developed for stochastic hybrid systems, it is the first fully automated model checking technique for stochastic timed automata. Using an implementation as part of the Modest Toolset and four varied examples, we show that the approach works in practice and present a detailed evaluation of its applicability, its efficiency, and current limitations
Verification of Information Flow Properties under Rational Observation
Get PDFInformation flow properties express the capability for an agent to infer information about secret behaviours of a partially observable system. In a language-theoretic setting, where the system behaviour is described by a language, we define the class of rational information flow properties (RIFP), where observers are modeled by finite transducers, acting on languages in a given family L. This leads to a general decidability criterion for the verification problem of RIFPs on L, implying PSPACE-completeness for this problem on regular languages. We show that most trace-based information flow properties studied up to now are RIFPs, including those related to selective declassification and conditional anonymity. As a consequence, we retrieve several existing decidability results that were obtained by ad-hoc proofs
Analysis of WIMP and Post WIMP Interactive Systems based on Formal Specification
Get PDFWhile designing interactive software, the use of a formal specification technique is of great help by providing non-ambiguous, complete and concise descriptions. The advantages of using such a formalism is widened if it is provided by formal analysis techniques that allow to prove properties about the design, thus giving an early verification to the designer before the application is actually implemented. This paper presents how models built using the Interactive Cooperative Objects formalism (ICOs) are amenable to formal verification. The emphasis is on the behavioral part of the description of the interactive systems and more precisely on the properties at the interaction technique level. However, the process and the associated tools can be generalized to the other parts of the interactive systems (including the non-interactive parts)
Exact and Approximate Abstraction for Classes of Stochastic Hybrid Systems
Get PDFA stochastic hybrid system contains a collection of interacting discrete and continuous components, subject to random behaviour. The formal verification of a stochastic hybrid system often comprises a method for the generation of a finite-state probabilistic system which either represents exactly the behaviour of the stochastic hybrid system, or which approximates conservatively its behaviour. We extend such abstraction-based formal verification of stochastic hybrid systems in two ways. Firstly, we generalise previous results by showing how bisimulation-based abstractions of non-probabilistic hybrid automata can be lifted to the setting of probabilistic hybrid automata, a subclass of stochastic hybrid systems in which probabilistic choices can be made with respect to finite, discrete alternatives only. Secondly, we consider the problem of obtaining approximate abstractions for discrete-time stochastic systems in which there are continuous probabilistic choices with regard to the slopes of certain system variables. We restrict our attention to the subclass of such systems in which the approximate abstraction of such a system, obtained using the previously developed techniques of Fraenzle et al., results in a probabilistic rectangular hybrid automaton, from which in turn a finite-state probabilistic system can be obtained. We illustrate this technique with an example, using the probabilistic model checking tool PRISM