Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Experimenting the Influence of Numerical Thresholds on Model-based Detection and Refactoring of Performance Antipatterns
Get PDFPerformance antipatterns are well-known bad design practices that lead to software products suffering from poor performance. A number of performance antipatterns has been defined and classified and refactoring actions have also been suggested to remove them. In the last few years, we have dedicated some effort to the detection and refactoring of performance antipatterns in software models.A specific characteristic of performance antipatterns is that they contain numerical parameters that may represent thresholds referring to either performance indices (e.g., a device utilization) or design features (e.g., number of interface operations of a software component). In this paper, we analyze the influence of such thresholds on the capability of detecting and refactoring performance antipatterns. In particular, (i) we analyze how a set of detected antipatterns may change while varying the threshold values and (ii) we discuss the influence of thresholds on the complexity of refactoring actions. With the help of a leading example, we quantify the influence using precision and recall metrics
QBF with Soft Variables
Get PDFQBF formulae are usually considered in prenex form, i.e. the quantifierblock is completely separated from the propositional part of the QBF.Among others, the semantics of the QBF is defined by the sequence ofthe variables within the prefix, where existentially quantifiedvariables depend on all universally quantified variables stated to theleft.In this paper we extend that classical definition and consider a newquantification type which we call soft variable. The idea is toallow a flexible position and quantifier type for these variables.Hence the type of quantifier of the soft variable can also bealtered. Based on this concept, we present an optimization problemseeking an optimal prefix as defined by user-given preferences. We statean algorithm based on MaxQBF, and present several applications – mainlyfrom verification area – which can be naturally translated into theoptimization problem for QBF with soft variables. We further implementeda prototype solver for this formalism, and compare our approach toprevious work, that differently from ours does not guarantee optimalityand completeness
Modelling Adaptive Networks: The Case of the Petrified Voters
Get PDFAdaptive networks are characterised by mutual dependencies between nodes' local state changes and evolving topology. Stochastic graph transformation systems are ideally suited to model such networks, but in order to analyse their properties we require more scalable methods. %We present a case study of a simple but representative example of adaptive networks. In this social network of opinionated voters a node connected to another of different opinion will either convert (changing state) or disconnect and establish a new connection with a node of the same opinion (changing topology). To analyse quantitative properties of the model, such as the long-term average ratio of edges connecting nodes of different opinions or the overall rate of change of opinions or connections, we use a refinement technique developed for the Kappa graph rewriting approach to derive a stochastic Petri net, replacing graphs as states by markings representing the frequency of occurrences of certain patterns. In general the number of patterns (and therefore places) is unbounded, but approximations can be used to replace complex patterns by combinations of simpler ones
Analysing Anti-patterns Static Relationships with Design Patterns
Get PDFAnti-patterns are motifs that are usually thought to be good solutions tosome design or implementation problems, but back-fires badly when applied. Previousstudies have reported that anti-patterns make object oriented systems hard tomaintain. Anti-patterns motifs usually have dependencies with other classes in thesystem. In this paper, we propose to analyse these dependencies (with in particulardesign patterns) in order to understand how developers can maintain programscontaining anti-patterns. To the best of our knowledge, no substantial investigationof anti-pattern dependencies with design patterns has been done before. This paperpresents the results of a study that we performed on three different systems, ArgoUML,JFreeChart, and XercesJ, written in Java, and of size ranges from 1,191to 3,325 classes, to analyse the static relationships between anti-patterns and designpatterns. We found that these relationships (1) exist, but (2) are temporaryand (3) classes participating in such relationships are more change-prone but lessfault-prone than other anti-pattern classes
Integrating model checking and UML based model-driven development for embedded systems
Get PDFThis paper discusses issues associated with integrating model checkers into a model-based development environment for embedded systems. The environment, DMOSES, is based on a formalization of UML Activity Diagrams and is used to generate correct and efficient code from such models; a key application area is the medical-device domain. A recent effort has focused on introducing formal reasoning into the development flow so that modelers can assess the correctness of their models before generating code from them. The verification of system requirements is shown using a case study of an infusion pump. This paper discusses issues involved in integrating model checkers into DMOSES and reports on a performance evaluation of two model checkers in particular: NuSMV and UPPAA
Clones and Macro co-changes
Get PDFIdeally, any change that modifies the similar parts of a cloned code snippet should be propagated to all its duplicates. In practice however, consistent propagation of changes in clones does not always happen. Current evidence indicates that clone families have a 50% chance of having consistent changes. This paper measures cloning and co-changes at file level as a proxy to assess the frequency of consistent changes. Given that changes to a clone group are not necessarily propagated in the same commit transaction (i.e., late propagations), our analysis uses macro co-changes instead of the traditional definition of co-changes. Macro changes group bursts of changes that are closer among themselves than to other changes, regardless of author or message. Then, macro co-changes are sets of files that change in the same macro changes. Each cloned file is tagged depending on whether any of the files with which it macro co-changes is cloned with it (during the macro change) or not. Contrary to previous results, we discovered that most of the cloned files macro co-change only with files with which they share clones. Thus providing evidence that macro changes are appropriate to study the conjecture of clones requiring co-changes, and indicating that consistent changes might be the norm in cloned code
Automated theorem proving for the systematic analysis of an infusion pump
Get PDFThis paper describes the use of an automated theorem prover to analyse properties of interactive behaviour. It offers an alternative to model checking for the analysis of interactive systems. There are situations, for example when demonstrating safety, in which alternative complementary analyses provide assurance to the regulator. The rigour and detail offered by theorem proving makes it possible to explore features of the design of the interactive system, as modelled, beyond those that would be revealed using model checking. Theorem proving can also speed up proof in some circumstances. The paper illustrates how a theory generated as a basis for theorem proving (using PVS) was developed systematically from a MAL model used to model check the same properties. It also shows how the CTL properties used to check the original model can be translated into theorems
Developing and Verifying User Interface Requirements for Infusion Pumps: A Refinement Approach
Get PDFIt is common practice in the description of criteria for the acceptable safety of systems for the regulator to describe safety requirements that should be satisfied by the system. These requirements are typically described precisely but in natural language and it is often unclear how the regulator can be assured that the given requirements are satisfied. This paper is concerned with a rigorous refinement process that demonstrates that a precise requirement is satisfied by the specification of a given device. It focuses on a particular class of requirements that relate to the user interface of the device. For user interface requirements, refinement is made more complex by the fact that systems can use different interaction devices that have very different characteristics. The described refinement process recognises an input/output hierarchy
Rapid Prototyping of Topology Control Algorithms by Graph Transformation
Get PDFTopology control algorithms are used to improve the energy efficiency (or other quality parameters) of wireless sensor networks. In this paper, we propose a model-driven rapid prototyping approach for the kTC topology control algorithm to enable the fast implementation and the evaluation of its different variants, and consequently, to accelerate the network quality experimentation cycle. In our approach, wireless sensor networks are described by graph-based models, and three variants of the kTC topology control algorithm are implemented by graph transformation, which are then executed on input network descriptions to derive modified topologies whose quality is then measured in several contexts to be able to assess the achieved network quality improvement
Automated Analysis of Voting Systems with Dolev-Yao Intruder Model
Get PDFThis paper presents a novel intruder model for automated reasoning about anonymity properties of voting systems. We adapt the lazy spy for this purpose, as it avoids the eagerness of pre-computation of unnecessary deductions, reducing the required state space for the analysis. This powerful intruder behaves as a Dolev-Yao intruder, which not only observes a protocol run, but also interacts with the protocol participants, overhears communication channels, intercepts and spoofs any messages that he has learned or generated from any prior knowledge. We make several important modifications in relation to existing channel types and the deductive system. For the former, we define various channel types for different threat models. For the latter, we construct a large deductive system over the space of messages transmitted in the voting system model. The model represents the first formal treatment of the vVote system, which is planned for use in 2014 in state elections in Victoria, Australia