@inproceedings{, author = {Bouchekir, Radouane and Guzman Cancimance, Michell and Alasdair, Cook and Haindl, Johannes and Woolnough, Riqaq}, title = {Formal Verification for Safe AI-based Flight Planning for UAVs}, booktitle = {2023 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W)}, publisher = {IEEE}, year = {2023}, month = jun, timestamp = 2023.06.27, abstract = {Planning and decision-making, especially the planning of collision-free paths, are an integral part of the operation of Unmanned Aerial Vehicles (UAVs). Formalisms like Temporal Plan Networks (TPN) can be used to provide optimal flight plans for UAVs. However, ensuring that the generated flight plans are safe can be a complex task, depending on the method used to generate the plans. Safe in this context means that the next planned action for the UAV does not violate safety constraints, for example, no-fly zones (NFZ). In this paper, we investigate the application of formal methods to generate metrics that could be used as assurance evidence in the argumentation of the safety of the planning component. In particular, we make use of Satisfiability Modulo Theories (SMT)-based verification to verify low-level requirements, together with Program Verification System (PVS) to check the design requirements of the AI-based planning component.}, isbn = {979-8-3503-2543-0}, issn = {2325-6664}, doi = {10.1109/DSN-W58399.2023.00068}, keywords = {Formal verification, theorem proving, SMT-based verification, Temporal plan network, Remotely Piloted Aircraft (RPA), Flight planning component.}, url = {https://ieeexplore.ieee.org/abstract/document/10207152}, } @inproceedings{VNC 2020, author = {Dantas, Yuri Gil and Nigam, Vivek and Talcott, Carolyn}, title = {A Formal Security Assessment Framework for Cooperative Adaptive Cruise Control}, booktitle = {IEEE Vehicular Networking Conference (VNC)}, publisher = {IEEE}, pages = {1-8}, year = {2020}, month = dec, abstract = {For increased safety and fuel-efficiency, vehicle platoons use Cooperative Adaptive Cruise Control (CACC) where vehicles adapt their state, incl. speed and position, based on information exchanged between vehicles. Intruders, however, may carry out attacks against CACC platoons by exploiting the communication channels used to cause harm, e.g., a vehicle crash. Therefore, during design-phase, engineers should provide evidence supporting platoon security. This paper proposes a formal framework for the security verification of CACC platoons to provide such evidence based on precise mathematical models. Our vehicle platoon models support the specification of both cyber, e.g., communication protocols, and physical, e.g., speeds, position, vehicle behaviors. Moreover, we propose intruder models that are parametric on his capabilities of manipulating communication channels, i.e., message injection and blocking. Our model is implemented enabling the automated formal verification involving both platoon and intruder models. We validate our machinery with a number of attacks taken from the literature and novel attacks discovered by using our formal machinery.}, doi = {10.1109/VNC51378.2020.9318334}, keywords = {attacks, formal verification, platoon, security, AutoFOCUS3, AF3}, } @article{, author = {Oakes, Bentley James and Troya, Javier and L{\'{u}}cio, Levi and Wimmer, Manuel}, title = {Full contract verification for ATL using symbolic execution}, journal = {Software & Systems Modeling}, volume = {17}, pages = {815--849}, year = {2018}, abstract = {The Atlas Transformation Language (ATL) is currently one of the most used model transformation languages and has become a de facto standard in model-driven engineering for implementing model transformations. At the same time, it is understood by the community that enhancing methods for exhaustively verifying such transformations allows for a more widespread adoption of model-driven engineering in industry. A variety of proposals for the verification of ATL transformations have arisen in the past few years. However, the majority of these techniques are either based on non-exhaustive testing or on proof methods that require human assistance and/or are not complete. In this paper, we describe our method for statically verifying the declarative subset of ATL model transformations. This verification is performed by translating the transformation (including features like filters, OCL expressions, and lazy rules) into our model transformation language DSLTrans. As we handle only the declarative portion of ATL, and DSLTrans is Turing-incomplete, this reduction in expressivity allows us to use a symbolic-execution approach to generate representations of all possible input models to the transformation. We then verify pre-/post-condition contracts on these representations, which in turn verifies the transformation itself. The technique we present in this paper is exhaustive for the subset of declarative ATL model transformations. This means that if the prover indicates a contract holds on a transformation, then the contract’s pre-/post-condition pair will be true for any input model for that transformation. We demonstrate and explore the applicability of our technique by studying several relatively large and complex ATL model transformations, including a model transformation developed in collaboration with our industrial partner. As well, we present our ‘slicing’ technique. This technique selects only those rules in the DSLTrans transformation needed for contract proof, thereby reducing proving time.}, doi = {10.1007/s10270-016-0548-7}, keywords = {Model transformation, ATL, Formal verification, Symbolic execution, Contracts, Pre-/post-conditions, Model-based Systems Engineering, MbSE}, } @inproceedings{DBLP:conf/models/KanavA17, author = {Kanav, Sudeep and Aravantinos, Vincent}, title = {Modular Transformation from {AF3} to nuXmv}, booktitle = {Proceedings of {MODELS} 2017 Satellite Event: Workshops (ModComp, ME, EXE, COMMitMDE, MRT, MULTI, GEMOC, MoDeVVa, MDETools, FlexMDE, MDEbug), Posters, Doctoral Symposium, Educator Symposium, {ACM} Student Research Competition, and Tools and Demonstrations}, pages = {300--306}, year = {2017}, abstract = {{AutoFOCUS3 (AF3)} supports formal verification of its models using the {nuXmv} model checker. This requires a model transformation from {AF3} to {nuXmv} models. In this paper we present this behavior transformation. It is a two way transformation between a high-level and a low-level model involving intricate cases typical of behavior transformations whose solutions can therefore be beneficial to the community.}, keywords = {AutoFOCUS3, formal verification, model-based systems engineering, MbSE}, url = {http://ceur-ws.org/Vol-2019/modevva_1.pdf}, crossref = {DBLP:conf/models/2017s}, } @inproceedings{8101258, author = {Aravantinos, Vincent and Kanav, Sudeep}, title = {Tool Support for Live Formal Verification}, booktitle = {2017 ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems (MODELS)}, pages = {145-155}, year = {2017}, abstract = {Despite an increasing interest from industry (e.g., DO333 standard [1]), formal verification is still not widely used in production for safety critical systems. This has been recognized for a while and various causes have been identified, one of them being the lack for scalable and cost effective tools. Many such tools exist for formal verification, but few of them are userfriendly: using formal verification generally still requires such an effort that the time spent on the tool prevents the integration of the method in an industrial setting. This paper presents a tool prototype aiming at supporting non-experts in using formal verification. The tooling approach is meant to be cost effective and change-supportive: user-friendliness is designed not only for the non-expert, but also to require minimum effort so that formal verification is triggered even for the non-enthusiast who is not willing to push a button. To do so, we trigger, in a background task, pre-defined formal verification checks at (almost) every change of the model. We only display error messages in case of problem: the user is not disturbed if no problem is detected. To prevent checks to be triggered all the time, we decide to consider only local analyses (i.e., only checks which do not require knowledge of elements in a remote position in the model). This restricts the sort of formal verification that we support, but this is a conscious choice: our motto is ”Let us first make basic techniques very user-friendly; more powerful ones will be considered only when at least the basic techniques have proven to be accepted”.}, doi = {10.1109/MODELS.2017.6}, keywords = {program verification, software tools, formal verification, safety critical systems, automata, component architectures, AutoFOCUS3, formal verification, model-based systems engineering, MbSE}, } @inproceedings{bytschkow2014, author = {Bytschkow, Denis and Quilbeuf, Jean and Igna, Georgeta and Rue{\ss}, Harald}, title = {Distributed MILS architectural approach for secure smart grids}, booktitle = {Smart Grid Security}, publisher = {Springer International Publishing}, pages = {16--29}, year = {2014}, month = aug, abstract = {Successful decentralized and prosumer-based smart grids need to be at least as dependable and secure as the prevailing one-way, generation-transmission-distribution-consumer power grids. With this motivation in mind, we propose a two-phase model-based design methodology for secure architectural design and secure deployment of such a security architecture on a distributed separation kernel. In particular, we are modeling essential parts of a smart micro grid with several interacting prosumers, and demonstrate exemplary security/privacy requirements of this smart grid. The security policy architecture of this smart grid is deployed on a secure distributed platform, relying on a combination of separation kernels and deterministic network, as developed in the Distributed MILS project.}, doi = {10.1007/978-3-319-10329-7_2}, keywords = {Smart grid security, Distributed MILS, Separation kernel, Formal verification, Security policy architecture, Configuration compiler, Model-based Systems Engineering, MbSE}, } @inproceedings{Teufl2014, author = {Teufl, Sabine and B{\"{o}}hm, Wolfgang and Pinger, Ralf}, title = {Understanding and closing the gap between requirements on system and subsystem level}, booktitle = {Model-Driven Requirements Engineering Workshop (MoDRE), 2014 IEEE 4th International}, pages = {77-86}, year = {2014}, month = aug, timestamp = 2014.09.23, owner = {teufl}, abstract = {In systems engineering, the increasing complexity of systems is handled by decomposing systems into subsystems. As part of the decomposition typically more abstract system requirements are refined to more detailed subsystem requirements. Refining system requirements to subsystem requirements includes the two steps interface refinement on the system boundaries, and a decomposition of system requirements to subsystem requirements. In order to apply formal analysis and verification techniques on the refinement of requirements, a formal refinement specification is necessary. In this paper we show the results of an exploratory industrial case study provided by Siemens, where we analyzed the refinement from system to subsystem requirements. We show that formal refinement specifications can become very complex, when interface refinement and requirement decompositions are performed in one step. In order to reduce complexity in the formal refinement specification, we introduce a formal restructuring approach for requirements. The main benefits of this restructuring approach are twofold. It enables reuse of requirements and knowledge preservation on the system level when the system architecture changes. Furthermore, quality assurance of the refinement on system level can now be performed independently from the system decomposition.}, doi = {10.1109/modre.2014.6890828}, keywords = {abstract system requirements, Abstracts, Analytical models, Case study, Complexity theory, formal analysis, formal refinement specification, formal restructuring approach, formal specification, formal verification, formal verification techniques, knowledge preservation, Modelling language, Quality assurance, Requirements engineering, requirements reuse, Siemens, subsystem requirements, Syntactics, system architecture, system decomposition, systems engineering}, } @inproceedings{, author = {Campetelli, Alarico and H{\"{o}}lzl, Florian and Neubeck, Florian}, title = {User-friendly Model Checking Integration in Model-based Development}, booktitle = {Proceedings of the 24th International Conference on Computer Applications in Industry and Engineering}, year = {2011}, abstract = {We present our approach to a user-friendly model checking integration in model-based development. The used modeling tool is AutoFocus 3, developed at our research group and specialized for reactive and embedded systems. For this integration, we approach usability at four points: tight coupling of verification properties with model elements, different specification languages for the formulation of properties, visualization of counterexamples as well as evaluation of different model checkers for adequate performance. Dealing with these issues leads to one of the first model-based development environments incorporating property specification, model checking and debugging.}, keywords = {verification, model checking, model-based development, tool support, embedded systems, AutoFOCUS3, formal verification, model-based systems engineering, MbSE}, }