IFIP Open Access Digital Library
Not a member yet
22614 research outputs found
Sort by
Interoperability for Emerging Technologies: A Systematic Scoping Review
No full textPart 6: Emerging TopicsInternational audienceInteroperability (IOP) is crucial for integrating emerging technologies (ETs) in the public sector, enabling efficient data exchange and interaction across various applications, systems, services, and organizations. Recognizing a gap in the systematic study of IOP’s role in the context of rapid technological advancements, this study employs a scoping review following PRISMA guidelines to identify key challenges and opportunities of IOP for adopting ETs in the public sector. Our analysis shows that a comprehensive approach to IOP is essential for maximizing the potential of ETs in the public sector. This approach promises to ensure smooth data exchange, effective system integration, stakeholder collaboration, legal and regulatory compliance, and enhanced public service provision. Our findings add to the ongoing discussion on digital transformation in the public sector, providing new insights into achieving a seamless technological ecosystem that integrates ETs and promotes innovative, efficient, and user-friendly public services
A Large Language Model Agent Based Legal Assistant for Governance Applications
No full textPart 4: AI in GovernmentInternational audienceLarge Language Models (LLMs) have gained significant traction, primarily due to their potential disruptive influence across industries reliant on natural language processing. Governance stands out as one such sector. Notably, there has been a surge in research activity surrounding the implications of LLMs in deciphering complex legal corpora. This research offers substantial assistance to various stakeholders, including decision-makers, administrators, and citizens. This article focuses on the design and implementation of an LLM-based legal assistant tailored for interacting with legal resources. To achieve this, a real-world scenario has been chosen, incorporating models GPT3.5 and GPT4 as the LLMs, a well-defined legal corpus comprising European Union (EU) legislation and case law concerning the General Data Protection Regulation (GDPR), alongside a series of reference legal queries of varying complexity. Retrieval Augmented Generation (RAG) as well as agent methodologies are employed to seamlessly integrate the LLMs’ functionalities with the customized dataset. The results appear to be promising, as the system managed to correctly address the majority of the legal queries, though with variable precision. Expectantly, the complexity of the queries severely impacted the quality of the outcome
Cognitively Available Cybersecurity: A Systematic Literature Review
No full textPart 2: Late-Breaking ResultsInternational audienceCybersecurity is imperative to safeguard the digital systems on which the world has come to rely. A core part of cybersecurity is users’ ability to adopt protective behavior by using security functions and adhering to security policies. Protective behavior requires cognitive effort, and some research suggests that users with cognitive challenges may struggle. There is no cohesive body of knowledge addressing those struggles and that gap is addressed in this research. A systematic literature was conducted to review how cognitive challenges are discussed in relationship to end-users’ cybersecurity. The findings reveal that the research on the topic is limited but agrees that adopting protective behavior is cognitively demanding. That hinders both users with cognitive disabilities and neurotypical users from being secure. While addressing cognitive challenges is the cybersecurity domain is identified as an important future challenge, limiting the effort put on users to minimize the required cognitive energy is identified as a starting point
Encoding Petri Nets into CCS
No full textPart 1: Regular PapersInternational audienceThis paper explores the problem of determining which classes of Petri nets can be encoded into behaviourally-equivalent CCS processes. Most of the existing related literature focuses on the inverse problem (i.e., encoding process calculi belonging to the CCS family into Petri nets), or extends CCS with Petri net-like multi-synchronisation (Multi-CCS). In this work, our main focus are free-choice and workflow nets (which are widely used in process mining to describe system interactions) and our target is plain CCS. We present several novel encodings, including one from free-choice workflow nets (produced by process mining algorithms like the α-miner) into CCS processes, and we prove that our encodings produce CCS processes that are weakly bisimilar to the original net. Besides contributing new expressiveness results, our encodings open a door towards bringing analysis and verification techniques from the realm of process calculi into the realm of process mining
Visualisation of Collective Systems with Sequit and Sibilla
No full textPart 4: Tool PapersInternational audienceThe analysis of Collective Systems involves the usage of several tools and techniques for addressing the different intricacies typical of this kind of system. One of these techniques is the simulation that, starting from a quantitative model of the system under analysis, is used to generate a set of possible computations. Typically, these data are used to perform statistical analyses and to infer performance measure. However, being able to represent results in an effective manner is crucial to help users to understand the meaning of collected simulation data. In this paper, we introduce Sequit a tool that, integrated with Sibilla, permits rendering in a 2D or 3D environment the evolution of a set of agents. A simple example, based on a flock behaviour, is used in the paper to show the use of Sibilla and Sequit
Modelling, Verifying and Testing the Contract Automata Runtime Environment with Uppaal
No full textPart 1: Regular PapersInternational audienceThe contract automata runtime environment (CARE) is a distributed middleware application recently introduced to realise service applications specified using a dialect of finite-state automata. In this paper, we detail the formal modelling and verification of CARE. We provide a formalisation as a network of stochastic timed automata. The model is verified against the desired properties with the tool Uppaal, utilizing exhaustive and statistical model checking techniques. This research emphasises the advantages of employing formal modelling, verification and testing processes to enhance the dependability of an open-source distributed application. We discuss the methodology used for modelling the application and address the issues that have been identified and fixed
Assessing Model Quality Using Large Language Models
No full textPart 2: Advances in Enterprise Modelling TechniquesInternational audienceRecently, researchers have explored whether large language models (LLMs) can be used as a substitute for domain experts to elicit information that should be represented in an enterprise model. This paper examines a slightly different application purpose, assessing an existing model’s quality using an LLM. We will analyze which aspects of model quality can be evaluated using an LLM in principle, referring to the established model quality framework SEQUAL. We will present a first test of assessing perceived semantic quality using ChatGPT. To examine the effect of different prompting strategies, we compared our results to the assessments of human domain experts. Our results suggest that LLMs are suitable for assessing the perceived semantic quality of models and provide a basis for considering further quality dimensions in future work
Explicit Hopcroft’s Trick in Categorical Partition Refinement
No full textInternational audienceAlgorithms for partition refinement are actively studied for a variety of systems, often with the optimisation called Hopcroft’s trick. However, the low-level description of those algorithms in the literature often obscures the essence of Hopcroft’s trick. Our contribution is twofold. Firstly, we present a novel formulation of Hopcroft’s trick in terms of general trees with weights. This clean and explicit formulation—we call it Hopcroft’s inequality—is crucially used in our second contribution, namely a general partition refinement algorithm that is functor-generic (i.e. it works for a variety of systems such as (non-)deterministic automata and Markov chains). Here we build on recent works on coalgebraic partition refinement but depart from them with the use of fibrations. In particular, our fibrational notion of R-partitioning exposes a concrete tree structure to which Hopcroft’s inequality readily applies. It is notable that our fibrational framework accommodates such algorithmic analysis on the categorical level of abstraction
Weak Simplicial Bisimilarity for Polyhedral Models and SLCS η
No full textPart 1: Full PapersInternational audienceIn the context of spatial logics and spatial model checking for polyhedral models — mathematical basis for visualisations in continuous space — we propose a weakening of simplicial bisimilarity. We additionally propose a corresponding weak notion of ±-bisimilarity on cell-poset models, discrete representation of polyhedral models. We show that two points are weakly simplicial bisimilar iff their representations are weakly ±-bisimilar. The advantage of this weaker notion is that it leads to a stronger reduction of models than its counterpart that was introduced in our previous work. This is important, since real-world polyhedral models, such as those found in domains exploiting mesh processing, typically consist of large numbers of cells. We also propose SLCS η, a weaker version of the Spatial Logic for Closure Spaces (SLCS) on polyhedral models, and we show that the proposed bisimilarities enjoy the Hennessy-Milner property: two points are weakly simplicial bisimilar iff they are logically equivalent for SLCS η. Similarly, two cells are weakly ±-bisimilar iff they are logically equivalent in the poset-model interpretation of SLCS η. This work is performed in the context of the geometric spatial model checker PolyLogicA and the polyhedral semantics of SLCS
Guess and Then Check: Controller Synthesis for Safe and Secure Cyber-Physical Systems
No full textPart 3: Short PapersInternational audienceIn this paper, we report our ongoing work on safe and secure controller synthesis for cyber-physical systems (CPS). Our approach separates the synthesis process into three phases, in which we alternatively perform exhaustive and selective exploration of the system’s state space. In this way, we combine the strengths of exhaustive search and learning to mitigate the state-space-explosion problem in controller synthesis while preserving the guarantee of safety and security. We implement the synthesis algorithms in the Rebeca (Reactive Objects Language) platform, which provides modelling, verification, and state-space visualization. We evaluate the new approach in an experiment, demonstrating the reduced number of explored states, which shows the potential of our approach for synthesizing safe and secure controllers for complex CPS