Abstract
This paper introduces a method to build dynamic logics with a graded semantics. The construction is parametrized by a structure to support both the spaces of truth and of the domain of computations. Possible instantiations of the method range from classical (assertional) dynamic logic to less common graded logics suitable to deal with programs whose transitional semantics exhibits fuzzy or weighted behaviour. This leads to the systematic derivation of program logics tailored to specific program classes.

Abstract
Dynamic logic combines logic with programs, which at a certain level of abstraction, can be regarded as behaviours changing the system state and, therefore, the truth value of formulas. This paper suggests a method for generating such logics for the domain of robot controllers and illustrates it with a logic for handling resource consumption.

Abstract
Continuous evolution towards very large, heterogeneous, highly dynamic computing systems entails the need for sound and flexible approaches to deal with system modification and re-engineering. The approach proposed in this paper combines an analysis stage, to identify concrete patterns of interaction in legacy code, with an iterative re-engineering process at a higher level of abstraction. Both stages are supported by the tools CoordPat and Archery, respectively. Bi-directional model transformations connecting code level and design level architectural models are defined. The approach is demonstrated in a (fragment of a) case study.

Abstract
Adding to the modal description of transition structures the ability to refer to specific states, hybrid(ised) logics provide an interesting framework for the specification of reconfigurable systems. The qualifier 'hybrid(ised)' refers to a generic method of developing, on top of whatever specification logic is used to model software configurations, the elements of an hybrid language, including nominals and modalities. In such a context, this paper shows how a calculus for a hybrid(ised) logic can be generated from a calculus of the base logic and that, moreover, it preserves soundness and completeness. A second contribution establishes that hybridising a decidable logic also gives rise to a decidable hybrid(ised) one. These results pave the way to the development of dedicated proof tools for such logics used in the design of reconfigurable systems.

Abstract
Architectural (bad) smells are design decisions found in software architectures that degrade the ability of systems to evolve. This paper presents an approach to verify that a software architecture is smell-free using the Archery architectural description language. The language provides a core for modelling software architectures and an extension for specifying constraints. The approach consists in precisely specifying architectural smells as constraints, and then verifying that software architectures do not satisfy any of them. The constraint language is based on a propositional modal logic with recursion that includes: a converse operator for relations among architectural concepts, graded modalities for describing the cardinality in such relations, and nominals referencing architectural elements. Four architectural smells illustrate the approach.

Abstract
In a reconfigurable system, the response to contextual or internal change may trigger reconfiguration events which, on their turn, activate scripts that change the system's architecture at runtime. To be safe, however, such reconfigurations are expected to obey the fundamental principles originally specified by its architect. This paper introduces an approach to ensure that such principles are observed along reconfigurations by verifying them against concrete specifications in a suitable logic. Architectures, reconfiguration scripts, and principles are specified in ARCHERY, an architectural description language with formal semantics. Principles are encoded as constraints, which become formulas of a two-layer graded hybrid logic, where the upper layer restricts reconfigurations, and the lower layer constrains the resulting configurations. Constraints are verified by translating them into logic formulas, which are interpreted over models derived from ARCHERY specifications of architectures and reconfigurations. Suitable notions of bisimulation and refinement, to which the architect may resort to compare configurations, are given, and their relationship with modal validity is discussed.