1,721,000 research outputs found
Special issue of the Journal of Symbolic Computation on Automated Specification and Verification of Web Systems
No full text
VERDI: an Automated Tool for Web sites Verification
No full textVERDI is a system for the automated verification of Web sites which can be used to specify integrity conditions for a given Web site, and then automatically check whether these conditions are actually fulfilled. It provides a rule-based, formal specification language which allows us to define syntactic/semantic properties of the Web site as well as a verification facility which computes the requirements not fulfilled by the Web site, and helps to repair the errors by finding out incomplete/missing Web pages
A Minimalist Visual Notation for Design Patterns and Antipatterns
No full textAchieving a quality software system requires UML designers to have a good understanding of both design patterns and antipatterns. Unfortunately, UML models for real systems tend to be huge and hard to manage, especially for models automatically generated from source code. Thus, it would be advisable to have tools to automatically identify particular instances of patterns. So, a formal language to express them is needed. However, a textual formalization of such a language is barely usable by UML practitioners. In this paper we propose a visual notation obtained by adding to UML as few graphical elements as possible in order to express both patterns and antipatterns (with the needed formality). As such additions are really few and intuitive, we believe that This approach has low cognitive load so is easily usable by practitioners but is still rigorous enough for implementation. This notation will be exploited by a GUI front-end for a prototypical tool (that we have recently developed) which is able to discover (anti)patterns in models
A rule-based method to match Software Patterns against UML Models
No full textAbstractIn a UML model, different aspects of a system are covered by different types of diagrams and this bears the risk that an overall system specification becomes barely tractable by the designer. When the model grows, it is likely that the architectural integrity will be compromised by extensions and bug-fixing operations. Hence, it is important to provide means to help designers to search in big models for particular instances of some variable schema of UML models (design patterns) they construct. This can help them both to find potential problems in the architecture design and to ensure that intended architectural choices had not been broken by mistake. In this paper we propose a rule-based method to find matches of design patterns into a UML model. The method is general enough to tackle most patterns and antipatterns
Specification and Verification of Web Applications in Rewriting Logic
No full textThis paper presents a Rewriting Logic framework that formalizes the interactions between Web servers and Web browsers through a communicating
protocol abstracting HTTP. The proposed framework includes a scripting language that is powerful enough to model the dynamics of complex Web
applications by encompassing the main features of the most popular Web scripting languages (e.g. PHP, ASP, Java Servlets). We also provide a
detailed characterization of browser actions (e.g. forward/backward navigation, page refresh, and new win- dow/tab openings) via rewrite rules,
and show how our models can be naturally model-checked by using the Linear Temporal Logic of Rewriting (LTLR), which is a Linear Temporal Logic
specifically designed for model-checking rewrite theories. Our formalization is particularly suit- able for verification purposes, since it allows
one to perform in-depth analyses of many subtle aspects related to Web interaction. Finally, the framework has been completely implemented in Maude,
and we report on some successful experiments that we conducted by using the Maude LTLR model-checker
Inferring Safe Maude Programs with ÁTAME
Full text linkIn this paper, we present \atame, an assertion-based program specialization tool for the multi-paradigm language Maude. The program specializer \atame\ takes as input a set \cA of system assertions that model the expected program behavior plus a Maude program \cR to be specialized that might violate some of the assertions in \cA. The outcome of the tool is a safe program refinement \cR' of \cR in which every computation is a good run, i.e., it satisfies the assertions in \cA. The specialization technique encoded in \atame\ is fully automatic and ensures that no good run of \cR is removed from \cR', while the number of bad runs is reduced to zero. We demonstrate the tool capabilities by specializing an overly general nondeterministic dam controller to fulfill a safety policy given by a set of system assertions
- …
