Model-driven transformations play a central role in MDE processes, yet their correctness is most often validated through testing or simulation. However, in contexts where critical scenarios may compromise system integrity or certification objectives, stronger guarantees are necessary. This paper investigates how the B method can support transformation engineering through verified formal specifications. To this end, we developed BCerT, an extension of the Meeduse language workbench, originally dedicated to the formal modeling of domain-specific languages. In our approach, transformations are defined as B operations or B events, allowing animation and model checking with ProB, as well as theorem proving with Atelier B. We discuss three complementary specification strategies: (i) a rule-oriented modeling approach optionally controlled with CSP||B; (ii) a property-driven operational B specification in which the transformation is expressed as a relation constrained by invariants; and (iii) an Event-B system capturing the transformation as atomic events focused on the end state. The approach is illustrated through two applications: the verification of a Truth Tables to Binary Decision Diagrams transformation presented at the Transformation Tool Contest, and the development of U2BCerT, a certified transpiler from UML state machines to Event-B.

Integrating access control into business processes is a non-trivial task. This paper presents an approach that combines the UML and B languages for the specification and validation of RBAC policies at the process level. It starts by modeling the access control rules using our extension of UML2 activity diagrams denominated as BAAC@UML (Business Activity Access Control with UML). The BAAC@UML models are then translated into a specification in the B language using our B4MSecure platform. Finally, the last step validates the RBAC policy by testing its formal specification using the B tools (Provers and Animators).

This paper evaluates the security specification techniques that employ Role Based Access Control (RBAC) variants. RBAC offers a special kind of access control mechanism based on the use of roles to grant permissions. Its variants include role hierarchy and separation of duty (SoD) constraints. The overall management of a RBAC supported system is made through its administrative, review and supporting system functions. In this paper, a summary of semi-formal and formal techniques employing RBAC is provided along with their benefits and limitations. Here, semi-formal techniques refer to UML+OCL while formal ones are based on Alloy. This paper may guide through the process of selecting an appropriate technique to specify security rules. This is done by analyzing the degree of coverage of RBAC including some extensions like SoD and role hierarchy. We also investigate the use of validation and verification tools in these techniques. We find that formal techniques are more amenable to automated analysis as compared to semi-formal ones. Semi-formal techniques are rich in specifying RBAC variants but have prototypic tools. Session based dynamic aspects of RBAC have been partly covered in both techniques.

Designing a security policy for an information system is a non-trivial task. In this paper, we consider the design of a security policy based on a variant of the RBAC model, close to SecureUML. This variant includes constraints for the separation of duty, as well as contextual constraints. Contextual constraints use information about the state of the functional model of the application to grant permissions to users. These constraints add flexibility to the security policy, but make its validation more difficult. In this paper, we first review two tools, USE and SecureMOVA, which can be used to analyse and validate a security policy. These tools focus on analyses of static aspects of the secured system. We then propose a new tool, based on the Z formal language, which uses animation of the specification to validate the static as well as dynamic aspects of the security policy, taking into account possible evolutions of the state of the functional model. We discuss how the security policy and the functional application are described to the tool, and what kind of queries and animations can be performed to analyse nominal and malicious behaviours of the system.

Nowadays, the Unified Modeling Language (UML) is becoming a "de facto" standard for object oriented environments and then it is perceived as a part of the culture of software engineers. However, the luck of rigorous semantic basis is a great shortcoming of UML which upsets its use to address safety problems. Still, taking benefit of the richness of UML to model critical systems is worthwhile because it is aimed at reducing the certification effort required for the design phase. Currently, we undertake works to delimit a well-defined UML core which could be used to model such systems. In this paper, we explore some critical aspects and recommendations of basic UML constructs which should be approached when dealing with safety.

Formal methods are nowadays the most rigorous way to produce software. However, the existing formal notations are not easy to use and understand for most people. Our approach proposes to circumvent this shortcoming by producing complementary graphical views on the formal developments. This paper addresses the graphical representation of formal B specifications using UML diagrams. A reverse-engineering approach is proposed to generate several class diagrams showing the static aspects of the B developments. These diagrams can help understand the specification for stakeholders who are not familiar with the B method, such as customers or certification authorities. A concept formation technique based on weighted link matrices is proposed to improve automation