Modelling and verifying smell-free architectures with the Archery language

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 smellfree 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.

On the verification of architectural reconfigurations

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.

Three-dimensional technology facilitates surgical performance of novice laparoscopy surgeons: a quantitative assessment on a porcine kidney model

Objective To determine whether the use of 3-dimensional (3D) imaging translates into a better surgical performance of naïve urologic laparoscopic surgeons during pyeloplasty (PY) and partial nephrectomy (PN) procedures. Materials and Methods Eighteen surgeons without any previous laparoscopic experience were randomly assigned to perform PY and PN in a porcine model using initially 2-dimensional (2D) and 3D laparoscopy. A surgical performance score was rated by an "expert" tutor through a modified 5-item global rating scale contemplating operative field view, bimanual dexterity, efficiency, tissue handling, and autonomy. Overall surgical time, complications, subjective perception of participating surgeons, and inconveniences related to the 3D vision were recorded. Results No difference in terms if operative time was found between 2D or 3D laparoscopy for both the PY (P =.51) and the PN (P =.28) procedures. A better rate in terms of surgical performance score was noted by the tutors when the study participants were using 3D vs 2D, for both PY (3.6 [0.8] vs 3.0 [0.4]; P =.034) and PN (3.6 [0.51] vs 3.15 [0.63]; P =.001). No complications occurred in any of the procedures. Most (77.2%) of the participating na??ve laparoscopic surgeons had the perception that 3D laparoscopy was overall easier than 2D. Headache (18.1%), nausea (18.1%), and visual disturbance (18.1%) were the most common issues reported by the surgeons during 3D procedures. Conclusion Despite the absence of translation in a shorter operative time, the use of 3D technology seems to facilitate the surgical performance of naive surgeons during laparoscopic kidney procedures on a porcine model.