Abstract Software architecture researchers have long assumed that architecture independent application descriptions can be mapped to architectures in many styles, that results vary in quality attributes, and that the choice of a style is driven by consideration of such attributes. In our previous work [1], we demonstrated the feasibility of formally treating architectural style as an independent variable. Given an application description and architectural style description in Alloy [3], we map them to software architecture description that refines the given application in conformance with the given style. To represent a map, we extend a traditional architectural style description (in Alloy) with predicates for mapping application descriptions in a given style to architectural descriptions in the given style. These predicates take application descriptions as parameters and define relationships required to hold between them and computed architectural descriptions. Given an application description, and a map, Alloy computes corresponding architectural descriptions guaranteed to conform to the given architectural style. This paper extends our earlier work to aspect-oriented structures. In doing so, we describe an aspect-enabled application description style and a map taking application descriptions in this style to pipe-and-filter architectures. We use the Alloy Analyzer to compute architecture descriptions, represented as satisfying solutions to the constraints of a map given an application description. The A2A transformer application, developed in our research group, then converts the Alloy-computed architecture to an architecture description in a traditional architecture description language (ADL): here, AspectualACME[2].
Abstract This paper presents AsmetaSMV, a model checker for Abstract State Machines (ASMs). It has been developed with the aim of enriching the ASMETA (ASM mETAmodeling) toolset – a set of tools for ASMs – with the capabilities of the model checker NuSMV to verify properties of ASM models written in the AsmetaL language. We describe the general architecture of AsmetaSMV and the process of automatically mapping ASM models into NuSMV programs. As a proof of concepts, we report the results of using AsmetaSMV to verify temporal properties of various case studies of different characteristics and complexity.
Abstract Scenario-driven requirement specifications are widely used to capture and represent high-level requirements. Timed Use Case Maps (TUCM) is a high-level scenario based modeling technique that can be used to capture and integrate behavioral and time-related aspects at a high level of abstraction. The Timed Use Case Maps language assumes durational semantics which introduces semantic variation points when dealing with concurrent flows. In this paper, we introduce three AsmL-based operational semantics, making the semantic variation points of TUCM concurrent behavior explicit. The proposed semantics are illustrated using an example.
Abstract Software development in B and Event-B generates proof obligations that have to be discharged using theorem provers. The cost of such developments therefore depends directly on the degree of automation and efficiency of theorem proving techniques for the logics in which these lemmas are expressed. This paper presents and formalizes an approach to transform a class of proof obligations generated in the Rodin platform in a language that can be addressed by state-of-the-art SMT solvers. The work presented in the paper handles proof obligations with Booleans, integer arithmetics and basic sets.
Abstract In a model-based testing approach as well as for the verification of properties by model-checking, B models provide an interesting solution. But for industrial applications, the size of their state space often makes them hard to handle. To reduce the amount of states, an abstraction function can be used, often combining state variable elimination and domain abstractions of the remaining variables. This paper illustrates a computer aided abstraction process that combines syntactic and semantic abstraction functions. The first function syntactically transforms a B event system M into an abstract one A, and the second one transforms a B event system into a Symbolic Labelled Transition System (SLTS). The syntactic transformation suppresses some variables in M. This function is correct in the sense that A is refined by M. A process that combines the syntactic and semantic abstractions has been experimented. It significantly reduces the time cost of semantic abstraction computation. This abstraction process allows for verifying safety properties by model-checking or for generating abstract tests. These tests are generated by a coverage criteria such as all states or all transitions of an SLTS.
Abstract We aim at extending the B language in order to build ASM programs which are correct with respect to B-like logical specifications. On the one hand, the main strengths of the B formal method are: i) the ability to express logical statements, and ii) the construction of a correct implementation by refinement. On the other hand, from our viewpoint, the striking aspects of ASM are the non-bounded outer loop that can reach the fixed point of a program and the power to express naturally any kind of (sequential) algorithms.
Abstract Scenarios have been used in various stages of the software development process, in particular in requirement elicitation and software validation and testing. In this paper, we present our recent work on the specification, design and implementation of a CoreASM plugin, called Bârun, that offers a powerful scripting language on top of the CoreASM extensible modeling framework and tool environment for high-level design and analysis of distributed systems. We illustrate the application of Bârun and demonstrate its features using an industrial case study.
Abstract There are two available approaches to automatically generate implementation code from timed automata model. The first approacch is implemented and attached to TIMES tool [1]. We will call this approach “TIMES approach”. While the second approach is based on using B-method [2] and its available code generation tool [3]. We will call this approach “B-method approach”. We select the model of the production cell to be used as a case study for the comparison between these two approaches. The same production cell model has been used against both approaches. The B-method approach generates platform independent code [4]. So we select the generated code using TIMES to be platform independent too for the comparison purpose. For the B-method approach, we use the deterministic semantic of timed automata which is used for TIMES code generation as given in [5]. This semantic controls the selection of the next executed function. The using of this deterministic mechanism is generally not needed for the code generated by the B-method approach. But we use it as it is the implemented mechanism for the TIMES approach. So we select to use it for comparison purpose. By running the implementation code generated using the B-method approach, it works fine as far as we run and no property violation could be found. On the other hand the code generated using TIMES approach runs successfully for the first 10 action transitions and then it progresses the time infinitely. This means that the system deadlocked, so it violates the first property of the model. While the first property is to guarantee that the system is deadlock free. This deadlock is due to the mishandling of the committed and urgent states [6]. The introduced comparison gave a result that the approach based on the using of B-method generates a verified code (by mean of simulation) and handles more timed automata features.
Abstract We investigate the use of ClawZ, a suite of tools for the verification of implementations of control laws, to construct formal models for control systems in the area of communications and signal-processing intensive applications. Whereas ClawZ has been successfully applied to verify control components in avionic systems, special requirements need to be identified and addressed to extend its use to the aforementioned application domain. This gives rise to several extensions, which we explain and subsequently validate by constructing the Z model of a software-defined radio communication device. The experience reported provides insight into general issues surrounding the use and extension of ClawZ.
Abstract We study the definition and the mapping of an AADL subset: the so called synchronous subset. We show that the data port protocol used for delayed and immediate connections between periodic threads can be interpreted in a synchronous way. In this paper, we formalize this interpretation and study the development of its mapping such that the original synchronous semantics is preserved. For that purpose, we use refinements through the Event B method.