44 research outputs found
To compose, or not to compose, that is the question:an analysis of compositional state space generation
No full text\u3cp\u3eTo combat state space explosion several compositional verification approaches have been proposed. One such approach is compositional aggregation, where a given system consisting of a number of parallel components is iteratively composed and minimised. Compositional aggregation has shown to perform better (in the size of the largest state space in memory at one time) than classical monolithic composition in a number of cases. However, there are also cases in which compositional aggregation performs much worse. It is unclear when one should apply compositional aggregation in favor of other techniques and how it is affected by action hiding and the scale of the model. This paper presents a descriptive analysis following the quantitiative experimental approach. The experiments were conducted in a controlled test bed setup in a computer laboratory environment. A total of eight scalable models with different network topologies considering a number of varying properties were investigated comprising 119 subjects. This makes it the most comprehensive study done so far on the topic. We investigate whether there is any systematic difference in the success of compositional aggregation based on the model, scaling, and action hiding. Our results indicate that both scaling up the model and hiding more behaviour has a positive influence on compositional aggregation.\u3c/p\u3
Lock and Fence When Needed: State Space Exploration + Static Analysis = Improved Fence and Lock Insertion
No full textVerifying a verifier: on the formal correctness of an LTS transformation verification technique
No full textOver the years, various formal methods have been proposed and further developed to determine the functional correctness of models of concurrent systems. Some of these have been designed for application in a model-driven development workflow, in which model transformations are used to incrementally transform initial abstract models into concrete models containing all relevant details. In this paper, we consider an existing formal verification technique to determine that formalisations of such transformations are guaranteed to preserve functional properties, regardless of the models they are applied on. We present our findings after having formally verified this technique using the Coq theorem prover. It turns out that in some cases the technique is not correct. We explain why, and propose an updated technique in which these issues have been fixed
Compositional model checking is lively
No full text\u3cp\u3eCompositional model checking approaches attempt to limit state space explosion by iteratively combining behaviour of some of the components in the system and reducing the result modulo an appropriate equivalence relation. For an equivalence relation to be applicable, it should be a congruence for parallel composition where synchronisations between the components may be introduced. An equivalence relation preserving both safety and liveness properties is divergence-preserving branching bisimulation (DPBB). It is generally assumed that DPBB is a congruence for parallel composition, even in the context of synchronisations between components. However, so far, no such results have been published. This work finally proves that this is the case. Furthermore, we discuss how to safely decompose an existing LTS network in components such that the re-composition is equivalent to the original LTS network. All proofs have been mechanically verified using the Coq proof assistant. Finally, to demonstrate the effectiveness of compositional model checking with intermediate DPBB reductions, we discuss the results we obtained after having conducted a number of experiments.\u3c/p\u3
A formal verification technique for behavioural model-to-model transformations
Get PDFIn Model Driven Software Engineering, models and model transformations are the primary artifacts when developing a software system. In such a workflow, model transformations are used to incrementally transform initial abstract models into concrete models containing all relevant system details. Over the years, various formal methods have been proposed and further developed to determine the functional correctness of models of concurrent systems. However, the formal verification of model transformations has so far not received as much attention. In this article, we propose a formal verification technique to determine that formalisations of such transformations in the form of rule systems are guaranteed to preserve functional properties, regardless of the models they are applied on. This work extends our earlier work in various ways. Compared to our earlier approaches, the current technique involves only up to n individual checks, with n the number of rules in the rule system, whereas previously, up to 2n − 1 checks were required. Furthermore, a full correctness proof for the technique is presented, based on a formal proof conducted with the Coq proof assistant. Finally, we report on two sets of conducted experiments. In the first set, we compared traditional model checking with transformation verification, and in the second set, we compared the verification technique presented in this article with the previous version
Method and apparatus for determining stress in an anatomical structure
Get PDF\u3cp\u3eA method of determining wall stress in an abdominal aortic aneurysm is disclosed. The method comprises determining, from anatomical image data, respective first stress values at locations on the wall, based on the aorta having substantially uniform stiffness. The primary direction of stress those locations are determined, and the locations of calcified regions (20) are then determined. The distance to the nearest calcified region is then determined for each location not corresponding to a calcified region, and the additional stress caused by the calcified regions is then determined from values stored in a memory.\u3c/p\u3
System and method for registration of medical images
No full textThe present invention relates to a system (1) and method for registration of medical image (10,11). Furthermore the invention relates to a computer program (5) for registration of medical images (10,11), when the computer program (5) is executed in a computer (2). In order to provide a more accurate registration transformation of medical images it is suggested to detect insufficiently similar areas (14,14',25,26) and to exclude them from the registration by means of an exclusion mask (22,24,27) that indicates which pixels/voxels should not be included during the registration process
Method and apparatus for determining stress in an anatomical structure
No full textA method of determining wall stress in an abdominal aortic aneurysm is disclosed. The method comprises determining, from anatomical image data, respective first stress values at locations on the wall, based on the aorta having substantially uniform stiffness. The primary direction of stress those locations are determined, and the locations of calcified regions (20) are then determined. The distance to the nearest calcified region is then determined for each location not corresponding to a calcified region, and the additional stress caused by the calcified regions is then determined from values stored in a memory.</p
Method and apparatus for determining stress in an anatomical structure
No full text\u3cp\u3eA method of determining wall stress in an abdominal aortic aneurysm is disclosed. The method comprises determining, from anatomical image data, respective first stress values at locations on the wall, based on the aorta having substantially uniform stiffness. The primary direction of stress those locations are determined, and the locations of calcified regions (20) are then determined. The distance to the nearest calcified region is then determined for each location not corresponding to a calcified region, and the additional stress caused by the calcified regions is then determined from values stored in a memory.\u3c/p\u3
