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. However, this approach is not common in formal methods development, which is generally high cost and time consuming, yet crucial in the development of critical systems. With the increase of more complex critical systems, it becomes more important to apply formal methods to the development cycle, and we propose a method that allows the application of SPL development techniques to formal methods. This results in faster and cheaper development of formal systems.
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. This kind of Services must verify the relevant constraints related to transactional systems. In our work, we focus on web services described with BPEL [1].
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. However, it is also important to show our techniques are sound with respect to standard model checking, at the algorithmic level. In this paper, we present a retrospective B development that addresses this issue through a series of B refinements. This work also demonstrates the valuable insights into a system that can be gained through formal modelling.
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. The larger problems are identifying and articulating critical properties, and ensuring that the components of a system - not only software modules, but also hardware peripherals, physical environments, and human operators - together establish them. Another common assumption is that verification must take system design and implementation as given. I’ll explain the rationale for, and elements of, a new approach to verification, in which design is driven by verification goals, and verification arguments are structured in a way that exposes the relationship between critical properties and the components that ensure them.
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. We present some use cases that exemplify this new feature and explain the applied heuristics. The NP-completeness nature of the verification problem makes hot core specially appealing, since it is quite frequent for users of the Alloy Analyzer to stop the analysis when some time threshold is exceeded. We provide experimental results showing very promising outcomes supporting our proposal.
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. Its graphical syntax and static semantics were defined following the “profile” extension mechanism of the UML metamodel, while its behavioral semantics was given in natural language. This paper provides a precise and executable semantics of the SystemC Process State Machines that are an extension of the UML state machines and are part of the SystemC UML profile to model the reactive behavior of the SystemC processes. To this purpose, we used the meta-hooking approach of the ASM-based semantic framework, which allows the definition of the dynamic semantics of metamodel-based languages and of UML profiles.
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. BSmart is a method and a corresponding tool designed to support the formal development of the complete Java Card smart card application, following the B formal method.