Abstract Feature-oriented modelling is a well-known approach for Software Product Line (SPL) development. It is a widely used method when developing groups of related software. With an SPL approach, the development of a software product is quicker, less expensive and of higher quality than a one-off development since much effort is re-used.
Abstract In software verification, scope-bounded checking of programs has become an effective technique for finding subtle bugs. Given bounds (that are iteratively relaxed) on input size and length of execution paths, a program and its correctness specifications are translated into a formula, which is solved using off-the-shelf solvers – a solution to the formula is a counterexample to the correctness specification.
Abstract The Service-Oriented Architectures (SOA) are increasingly used in various application domains. Nowadays various Services operate on the Web and access various critical resources such as databases. These services are called transactional web services when they perform transactional actions.
Abstract Symmetry reduction is a model checking technique that can help alleviate the problem of state space explosion, by preventing redundant state space exploration. In previous work, we have developed three effective approaches to symmetry reduction for B that have been implemented into the ProB model checker, and we have proved the soundness of our state symmetries.
Abstract How should a software system be verified? Much research is currently focused on attempts to show that code modules meet their specifications. This is important, but bugs in code are not the weakest link in the chain.
Abstract Identifying a minimal unsatisfiable core in an Alloy model proved to be a very useful feature in many scenarios. We extend this concept to hot core, an approximation to unsat core that enables the user to obtain valuable feedback when the Alloy’s sat-solving process is abruptly interrupted.
Abstract The SystemC UML profile is a modeling language designed to lift features and abstractions of the SystemC/C++ class library to the UML level with the aim of improving the current industrial System-on-Chip design methodology.
Abstract We extend the Alloy language with the standard imperative constructs; we show the mix of declarative and imperative constructs to be useful in modeling dynamic systems. We present a translation from our extended language to the existing first-order logic of the Alloy Analyzer, allowing for efficient analysis of models.
Abstract Smart Card applications usually require reliability and security to avoid incorrect operation or access violation in transactions and corruption or undue access to stored information. A way of reaching these requirements is improving the quality of the development process of these applications.
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.
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.
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.
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.
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.
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.
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.
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”.
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.
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.
Abstract We present here a case study developing a parallel program. The approach that we use combines refinement and decomposition techniques. This involves in the first step to abstractly specify the aim of the program, then subsequently introduce shared information between sub-processes via refinement.
Abstract Software engineering diagrams are hard to verify and formally analyse, often due to inadequately defined diagram semantics: the semantics often does not enable formal analysis, or may be under specified to a degree that does not allow useful properties to be checked.
Abstract Traditionally, simulation is used to perform probabilistic analysis. However, it provides less accurate results and cannot handle large-scale problems due to the enormous CPU time requirements. Recently, a significant amount of formalization has been done in higher-order logic that allows us to conduct precise probabilistic analysis using theorem proving and thus overcome the limitations of the simulation.
Abstract The topic of access control has received a new lease of life in recent years as the need for assurance that the correct access control policy is in place is seen by many as crucial to providing assurance to individuals that their data is being treated appropriately.
Abstract The aim of this paper is to give some feedback about the B specification [1] of a localization software component which is one of the most critical parts in the land transportation system.
Abstract An important frequent task in both Z and B is the proof of verification conditions (VCs). In Z and B, VCs can be predicates to be discharged as a result of refinement steps, some proof about initialization properties or domain checking.
Abstract While several different techniques utilize specifications to check correctness of programs before they are deployed, the use of specifications in deployed software is more limited, largely taking the form of runtime checking where assertions form a basis for detecting erroneous program states and terminating erroneous executions in failures.
Abstract The Java programming language has been widely described as secure by design. Nevertheless, a number of serious security vulnerabilities have been discovered in Java, particularly in the component known as the Bytecode Verifier.
Abstract This paper presents Matelas, a B predicate calculus definition for social networking, modelling social-network content, privacy policies, social-networks friendship relations, and how these relations effect users’ policies. The work presented in this paper is part of an ongoing work that aims at using several formal methods tools and techniques to develop a full-fledged social-network service implementing stipulated policies.
Abstract Event-B [1] is a formalism for discrete system modelling. The Rodin platform [2] provides a toolset to carry out specification, refinement and proof in Event-B. The importance of proofs as part of formal modelling cannot be emphasised enough, and as such, it is imperative to provide effective tool support for it.