1,721,038 research outputs found
Specification and animation of security design models using Z
No full textL'écriture de spécifications pour des logiciels en général et en particulier pour des applications sécurisées demande de développer des techniques qui facilitent la détection et la prévention des erreurs de conception, dès les premières phases du développement. Ce besoin est motivé par les coûts et délais des phases de vérification et validation. De nombreuses méthodes de spécification, tant formelles qu'informelles ont été proposées et, comme nous le verrons dans cette thèse, les approches formelles donnent des spécifications de meilleure qualité.L'ingénierie des systèmes sécurisés propose l'utilisation de modèles de conception de la sécurité pour représenter les applications sécurisées. Dans de nombreux cas, ces modèles se basent sur les notations graphiques d'UML avec des extensions, sous forme de profils comme SecureUML, pour exprimer la sécurité. Néanmoins, les notations d'UML, même étendues avec des assertions OCL, sont insuffisantes pour garantir la correction de ces modèles. Ceci est notamment du aux limites des outils d'animation utilisés pour valider des modèles UML étendus en OCL. Nous proposons de combiner des langages formels comme Z avec UML pour valider des applications en animant leurs spécifications, indépendamment de futurs choix d'implémentation. Le but de cette thèse est de présenter une approche pour analyser par animation des modèles de conception de la sécurité. Nous utilisons un outil pré-existant, RoZ, pour traduire les aspects fonctionnels du modèle UML en Z. Cependant, RoZ ne couvre pas la modélisation des aspects sécuritaires. Dans cette thèse, nous avons complété l'outil RoZ en l'associant à un noyau de sécurité qui spécifie les concepts du modèle RBAC (Role Based Access Control). Nous utilisons l'animation pour explorer dynamiquement et ainsi valider les aspects sécuritaires de l'application.Notre approche et les outils qui la supportent intègrent UML, SecureUML (un langage de modélisation de la sécurité), RBAC, RoZ, Z et Jaza, un animateur pour le langage Z. L'animation des spécifications prend la forme de scénarios définis par l'utilisateur qui permettent de se convaincre que la spécification décrit correctement ses besoins. Notre approche permet une validation dès la phase de spécification, qui prend en considération l'interaction entre les modèles fonctionnel et sécuritaire, et qui fait abstraction des choix de l'implémentation. Les éléments du modèle fonctionnel peuvent être utilisés comme contexte dans la définition des permissions du modèle de sécurité. Notre approche ne met pas de contrainte sur ce modèle fonctionnel ce qui permet de l'utiliser pour une vaste gamme d'applications.Specifying security-critical software urges to develop techniques that allow early bugs detection and prevention. This is aggravated by the fact that massive cost and time are spent during product validation and verification (V&V). There exists a multitude of formal and informal techniques striving to confront the challenge of specifying and validating specifications. Our approach mainly concerns validating the security specifications by animating the formal models, which adds a new dimension to the state-of-the-art.Secure system engineering dedicated to tackle security features offers security-design models to sketch secure applications. Generally for these, Unified Modeling Language (UML) is considered a de facto standard along with a few extensions such as SecureUML and Object Constraint Language (OCL). OCL tends to add precision in design but yet it remains far from obtaining bugs free specifications. One reason to that is the inability of the OCL-based techniques to animate models before proceeding to an implementation.Combining formal languages such as Z with UML allows applying animation techniques enabling early validation of software design. The RoZ tool is capable of translating UML models into the Z specifications which further can be verified or validated. But RoZ is lacking to provide similar features for secure applications. In this thesis, we have upgraded this tool using an underlying security kernel backed up by Role Based Access Control (RBAC). Our approach not only allows validating the specifications but can animate the formal models. The animation also takes into account both the static and the dynamic aspects (i.e., session management) of RBAC-based security policies. Our unified approach and toolset involves a systematic usage and linkage of UML, SecureUML, RBAC, RoZ, Z, and the Just Another Z Animator (Jaza) tool. Using Jaza, the sort of validation we perform allows enumerating user defined scenarios to determine if the specification describes the intended reality. We emphasize on simultaneous consideration of functional and non-functional properties and consider functional models as contextual constraints over the security models. From a user viewpoint, our proposed approach can arbitrarily be composed with any functional model to examine an RBAC-based security policy
Ingénierie Formelle Dirigée par les Modèles
No full textMy research works are dedicated to the integration of two well known paradigms: Formal Methods (FM) and Model-Driven Engineering (MDE). This integration is called Formal MDE (FMDE) all along the current document. In fact, several works have been already done in order to strengthen the MDE paradigm with formal reasoning, and therefore make it more viable as far as safety and security concerns have to be addressed. When taken separately, these works provide a partial coverage of MDE, but when combined they can address a wide range of models and languages. During the last decade, I investigated two directions in which the FMDE paradigm proved its value: (\emph{i})~Model-Driven Security~(MDS), and (\emph{ii})~Domain-Specific Languages~(DSLs). Under the MDE umbrella, both the MDS and DSL communities advocate for the use of models throughout the development process, providing solutions to the validation problem (`\emph{do the right system}'). Nonetheless, the verification problem (`\emph{do the system right}') is still a major challenge, perhaps because formal reasoning (\emph{i.e.}~model-checking and/or theorem proving) was not apart of the MDE initiative. To be pragmatic my contributions build on well-established notations: mainly UML and B, and at a smaller scale BPMN, CSP, Z and Petri-Nets. Besides, the obtained results can be inspiring and, in my opinion, should be extended with other (semi-)formal languages, which would confer to FMDE a broader spectrum. This document summarizes for every research direction (respectively MDS and DSLs) the challenges that guided my works, and give an overview of my contributions and publications in the field
B/UML : Mise en relation de spécifications B et de descriptions UML pour l'aide à la validation externe de développements formels en B.
No full textThe complex requirements of software systems justify the use of the best existing techniques to guarantee the quality of specifications and to preserve this quality during the programming phase of a software life-cycle. Formal methods, such as B, make it possible to reach such a level of quality. However, there is a cultural gap between formal methods, with their mathematical concepts and notations, and the usual techniques of the various stakeholders in industrial projects (graphical formalisms and natural language documents). There is thus a significant risk that errors such as misinterpretation of the requirements and specification documents lead to erroneously validate the specification, and hence to produce the wrong system. So, software specification and development tools, which combine formal and graphical methods widely used in industrial projects, such as B and UML, are likely of a great importance. In this work we focus our interest on the B method which is a formal method used to model systems and prove their correctness by successive refinements. Our goal is to produce graphical UML views from existing formal B specifications in order to ease their readability and then help their external validation. In fact, such views can be useful for various stakeholders in a formal development process : they are intended to support the understanding of the formal specifications by the requirements holders and the certification authorities ; they can also be used by the B developers to get an alternate view on their work. We centered the derivation of UML class diagrams from B specifications on a reverse-engineering technique guided by a set of structural and semantic mappings specified on a meta-level. The derivation of state/transition diagrams is based on an abstraction technique applied to accessibility graphs which are built by an exhaustive unfolding of the behavior of B specifications.Les exigences qui s'appliquent aux composants logiciels et aux logiciels embarqués justifient l'utilisation des meilleures techniques disponibles pour garantir la qualité des spécifications et conserver cette qualité lors du développement du code. Les méthodes formelles, et parmi elles la méthode B, permettent d'atteindre ce niveau de qualité. Cependant, ces méthodes utilisent des notations et des concepts spécifiques, qui génèrent souvent une faible lisibilité et une difficulté d'intégration dans les processus de développement et de certification. Ainsi, proposer des environnements de spécification, de développement de programmes et de logiciels, combinant des méthodes formelles et des méthodes semi-formelles largement utilisées dans les projets industriels, en l'occurrence B et UML, s'avère d'une grande importance. Notre intérêt porte précisément sur la méthode B qui est une méthode formelle utilisée pour modéliser des systèmes et prouver l'exactitude de leur conception par raffinements successifs. Mais les spécifications formelles sont difficiles à lire quand elles ne sont pas accompagnées d'une documentation. Cette lisibilité est essentielle pour une bonne compréhension de la spécification, notamment dans des phases de validation ou de certification. Aujourd'hui, en B, cette documentation est fournie sous forme de texte, avec, quelquefois, des schémas explicitant certaines caractéristiques du système. L'objectif de ce travail de thèse est de mettre en relation des spécifications en B avec des diagrammes UML, qui constituent un standard de facto dans le monde industriel et dont le caractère graphique améliore la lisibilité. Nous avons axé notre processus de dérivation de diagrammes de classes à partir de spécifications B autour d'une technique d'ingénierie inverse guidée par un ensemble de correspondances structurelles et sémantiques spécifiées à un méta-niveau. Quant à la dérivation de diagrammes d'états/transitions, elle a été orientée vers une technique d'abstraction de graphes d'accessibilité construits par une exploration exhaustive du comportement de la spécification
Ingénierie Formelle Dirigée par les Modèles
No full textMy research works are dedicated to the integration of two well known paradigms: Formal Methods (FM) and Model-Driven Engineering (MDE). This integration is called Formal MDE (FMDE) all along the current document. In fact, several works have been already done in order to strengthen the MDE paradigm with formal reasoning, and therefore make it more viable as far as safety and security concerns have to be addressed. When taken separately, these works provide a partial coverage of MDE, but when combined they can address a wide range of models and languages. During the last decade, I investigated two directions in which the FMDE paradigm proved its value: (\emph{i})~Model-Driven Security~(MDS), and (\emph{ii})~Domain-Specific Languages~(DSLs). Under the MDE umbrella, both the MDS and DSL communities advocate for the use of models throughout the development process, providing solutions to the validation problem (`\emph{do the right system}'). Nonetheless, the verification problem (`\emph{do the system right}') is still a major challenge, perhaps because formal reasoning (\emph{i.e.}~model-checking and/or theorem proving) was not apart of the MDE initiative. To be pragmatic my contributions build on well-established notations: mainly UML and B, and at a smaller scale BPMN, CSP, Z and Petri-Nets. Besides, the obtained results can be inspiring and, in my opinion, should be extended with other (semi-)formal languages, which would confer to FMDE a broader spectrum. This document summarizes for every research direction (respectively MDS and DSLs) the challenges that guided my works, and give an overview of my contributions and publications in the field
Going Beyond Counting First Authors in Author Co-citation Analysis
Get PDFThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
A Lightweight Development of Outbreak Prevention Strategies Built on Formal Methods and xDSLs
No full textInternational audienc
Transpilation of Petri-nets into B
No full textInternational audiencePetri-nets and their variants (Place/Transition nets, High-Level Petri Nets, etc.) are widely used in the development of safety critical-systems. Their success is related to three major aspects: a formal semantics, a graphical syntax and the availability of verification tools. In our previous work we presented a new vision for the semantic definition of Petri-nets applying a Formal Model-Driven Engineering (FMDE) built on the B method. The approach is powered by Meeduse, a language workbench that we developed in order to formally instrument executable Domain-Specific Languages (xDSLs) by applying a deep embedding technique and the B method. However, because of the abstract nature of the underlying formal models, our deep embedding is suitable for the validation and verification activities at the design stage but not sufficient to generate code for target platforms. This paper advances our previous work with a shallow embedding technique taking benefit of the B method tools in order to safely synthesize executable Petri-net controllers that can be embedded in target platforms
The B Method Meets MDE: Review, Progress and Future
No full textInternational audienceExisting surveys about language workbenches (LWBs) ranging from 2006 to 2019 observe a poor usage of formal methods within domain-specific languages (DSLs) and call for identifying the reasons. We believe that the lack of automated formal reasoning in LWBs, and more generally in MDE, is not due to the complexity of formal methods and their mathematical background, but originates from the lack of initiatives that are dedicated to the integration of existing tools and techniques. To this aim we developed the Meeduse LWB and investigated the use of the B method to rigorously define the semantics of DSLs. The current applications of Meeduse show that the integration of DSLs together with theorem proving, animation and model-checking is viable and should be explored further. This technique is especially interesting for executable DSLs (xDSLs), which are DSLs with behavioural features. This paper is a review of our Formal MDE (FMDE) approach for xDSLs and a proposal for new avenues of investigation
- …
