-
WeakSATD: Detecting Weak Self-admitted Technical Debt
Authors:
Barbara Russo,
Matteo Camilli,
Moritz Mock
Abstract:
Speeding up development may produce technical debt, i.e., not-quite-right code for which the effort to make it right increases with time as a sort of interest. Developers may be aware of the debt as they admit it in their code comments. Literature reports that such a self-admitted technical debt survives for a long time in a program, but it is not yet clear its impact on the quality of the code in…
▽ More
Speeding up development may produce technical debt, i.e., not-quite-right code for which the effort to make it right increases with time as a sort of interest. Developers may be aware of the debt as they admit it in their code comments. Literature reports that such a self-admitted technical debt survives for a long time in a program, but it is not yet clear its impact on the quality of the code in the long term. We argue that self-admitted technical debt contains a number of different weaknesses that may affect the security of a program. Therefore, the longer a debt is not paid back the higher is the risk that the weaknesses can be exploited. To discuss our claim and rise the developers' awareness of the vulnerability of the self-admitted technical debt that is not paid back, we explore the self-admitted technical debt in the Chromium C-code to detect any known weaknesses. In this preliminary study, we first mine the Common Weakness Enumeration repository to define heuristics for the automatic detection and fix of weak code. Then, we parse the C-code to find self-admitted technical debt and the code block it refers to. Finally, we use the heuristics to find weak code snippets associated to self-admitted technical debt and recommend their potential mitigation to developers. Such knowledge can be used to prioritize self-admitted technical debt for repair. A prototype has been developed and applied to the Chromium code. Initial findings report that 55\% of self-admitted technical debt code contains weak code of 14 different types.
△ Less
Submitted 4 May, 2022;
originally announced May 2022.
-
Collaborative Artificial Intelligence Needs Stronger Assurances Driven by Risks
Authors:
Jubril Gbolahan Adigun,
Matteo Camilli,
Michael Felderer,
Andrea Giusti,
Dominik T Matt,
Anna Perini,
Barbara Russo,
Angelo Susi
Abstract:
Collaborative AI systems (CAISs) aim at working together with humans in a shared space to achieve a common goal. This critical setting yields hazardous circumstances that could harm human beings. Thus, building such systems with strong assurances of compliance with requirements, domain-specific standards and regulations is of greatest importance. Only few scale impact has been reported so far for…
▽ More
Collaborative AI systems (CAISs) aim at working together with humans in a shared space to achieve a common goal. This critical setting yields hazardous circumstances that could harm human beings. Thus, building such systems with strong assurances of compliance with requirements, domain-specific standards and regulations is of greatest importance. Only few scale impact has been reported so far for such systems since much work remains to manage possible risks. We identify emerging problems in this context and then we report our vision, as well as the progress of our multidisciplinary research team composed of software/systems, and mechatronics engineers to develop a risk-driven assurance process for CAISs.
△ Less
Submitted 22 September, 2022; v1 submitted 1 December, 2021;
originally announced December 2021.
-
Towards Risk Modeling for Collaborative AI
Authors:
Matteo Camilli,
Michael Felderer,
Andrea Giusti,
Dominik T. Matt,
Anna Perini,
Barbara Russo,
Angelo Susi
Abstract:
Collaborative AI systems aim at working together with humans in a shared space to achieve a common goal. This setting imposes potentially hazardous circumstances due to contacts that could harm human beings. Thus, building such systems with strong assurances of compliance with requirements domain specific standards and regulations is of greatest importance. Challenges associated with the achieveme…
▽ More
Collaborative AI systems aim at working together with humans in a shared space to achieve a common goal. This setting imposes potentially hazardous circumstances due to contacts that could harm human beings. Thus, building such systems with strong assurances of compliance with requirements domain specific standards and regulations is of greatest importance. Challenges associated with the achievement of this goal become even more severe when such systems rely on machine learning components rather than such as top-down rule-based AI. In this paper, we introduce a risk modeling approach tailored to Collaborative AI systems. The risk model includes goals, risk events and domain specific indicators that potentially expose humans to hazards. The risk model is then leveraged to drive assurance methods that feed in turn the risk model through insights extracted from run-time evidence. Our envisioned approach is described by means of a running example in the domain of Industry 4.0, where a robotic arm endowed with a visual perception component, implemented with machine learning, collaborates with a human operator for a production-relevant task.
△ Less
Submitted 12 March, 2021;
originally announced March 2021.
-
Constructing Coverability Graphs for Time Basic Petri Nets
Authors:
Matteo Camilli
Abstract:
Time-Basic Petri nets, is a powerful formalism for modeling real-time systems where time constraints are expressed through time functions of marking's time description associated with transition, representing possible firing times. We introduce a technique for coverability analysis based on the building of a finite graph. This technique further exploits the time anonymous concept [5,6], in order t…
▽ More
Time-Basic Petri nets, is a powerful formalism for modeling real-time systems where time constraints are expressed through time functions of marking's time description associated with transition, representing possible firing times. We introduce a technique for coverability analysis based on the building of a finite graph. This technique further exploits the time anonymous concept [5,6], in order to deal with topologically unbounded nets, exploits the concept of a coverage of TA tokens, i.e., a sort of ω anonymous timestamp. Such a coverability analysis technique is able to construct coverability trees/graphs for unbounded Time-Basic Petri net models. The termination of the algorithm is guaranteed as long as, within the input model, tokens growing without limit, can be anonymized. This means that we are able to manage models that do not exhibit Zeno behavior and do not express actions depending on infinite past events. This is actually a reasonable limitation because, generally, real-world examples do not exhibit such a behavior.
△ Less
Submitted 19 September, 2014;
originally announced September 2014.
-
Verification of Reachability Problems for Time Basic Petri Nets
Authors:
Matteo Camilli
Abstract:
Time-Basic Petri nets, is a powerful formalism for model- ing real-time systems where time constraints are expressed through time functions of marking's time description associated with transition, representing possible firing times. We introduce a technique for reachability analysis based on the building of finite contraction of the infinite state space associated with such a models. The techniqu…
▽ More
Time-Basic Petri nets, is a powerful formalism for model- ing real-time systems where time constraints are expressed through time functions of marking's time description associated with transition, representing possible firing times. We introduce a technique for reachability analysis based on the building of finite contraction of the infinite state space associated with such a models. The technique constructs a finite symbolic reachability graph relying on a sort of time coverage, and over- comes the limitations of the existing available analyzers for Time-Basic nets, based in turn on a time-bounded inspection of a (possibly infinite) reachability-tree. A key feature of the technique is the introduction of the Time Anonymous concept, which allows the identification of components not influencing the evolution of a model. A running example is used throughout the paper to sketch the symbolic graph construction. The graph construction algorithm has been automated by a Java tool-set, described in the paper together with its main functionality and analysis capability. A use case describing a real-world example has been employed to benchmark the technique and the tool-set. The main outcome of this test are also presented in the paper.
△ Less
Submitted 9 September, 2014;
originally announced September 2014.
-
Distributed CTL Model Checking in the Cloud
Authors:
Carlo Bellettini,
Matteo Camilli,
Lorenzo Capra,
Mattia Monga
Abstract:
The recent extensive availability of "big data" platforms calls for a more widespread adoption by the formal verification community. In fact, formal verification requires high performance data processing software for extracting knowledge from the unprecedented amount of data which come from analyzed systems. Since cloud based computing resources have became easily accessible, there is an opportuni…
▽ More
The recent extensive availability of "big data" platforms calls for a more widespread adoption by the formal verification community. In fact, formal verification requires high performance data processing software for extracting knowledge from the unprecedented amount of data which come from analyzed systems. Since cloud based computing resources have became easily accessible, there is an opportunity for verification techniques and tools to undergo a deep technological transition to exploit the new available architectures. This has created an increasing interest in parallelizing and distributing verification techniques. In this paper we introduce a distributed approach which exploits techniques typically used by the "big data" community to enable verification of Computation Tree Logic (CTL) formulas on very large state spaces using distributed systems and cloud computing facilities. The outcome of several tests performed on benchmark specifications are presented, thus showing the convenience of the proposed approach.
△ Less
Submitted 24 October, 2013;
originally announced October 2013.
-
State Space Exploration of RT Systems in the Cloud
Authors:
Carlo Bellettini,
Matteo Camilli,
Lorenzo Capra,
Mattia Monga
Abstract:
The growing availability of distributed and cloud computing frameworks make it possible to face complex computational problems in a more effective and convenient way. A notable example is state-space exploration of discrete-event systems specified in a formal way. The exponential complexity of this task is a major limitation to the usage of consolidated analysis techniques and tools. We present an…
▽ More
The growing availability of distributed and cloud computing frameworks make it possible to face complex computational problems in a more effective and convenient way. A notable example is state-space exploration of discrete-event systems specified in a formal way. The exponential complexity of this task is a major limitation to the usage of consolidated analysis techniques and tools. We present and compare two different approaches to state-space explosion, relying on distributed and cloud frameworks, respectively. These approaches were designed and implemented following the same computational schema, a sort of map & fold. They are applied on symbolic state-space exploration of real-time systems specified by (a timed extension of) Petri Nets, by readapting a sequential algorithm implemented as a command-line Java tool. The outcome of several tests performed on a benchmarking specification are presented, thus showing the convenience of cloud approaches.
△ Less
Submitted 30 March, 2012;
originally announced March 2012.
-
Preserving Co-Location Privacy in Geo-Social Networks
Authors:
Matteo Camilli
Abstract:
The number of people on social networks has grown exponentially. Users share very large volumes of personal informations and content every days. This content could be tagged with geo-spatial and temporal coordinates that may be considered sensitive for some users. While there is clearly a demand for users to share this information with each other, there is also substantial demand for greater contr…
▽ More
The number of people on social networks has grown exponentially. Users share very large volumes of personal informations and content every days. This content could be tagged with geo-spatial and temporal coordinates that may be considered sensitive for some users. While there is clearly a demand for users to share this information with each other, there is also substantial demand for greater control over the conditions under which their information is shared. Content published in a geo-aware social networks (GeoSN) often involves multiple users and it is often accessible to multiple users, without the publisher being aware of the privacy preferences of those users. This makes difficult for GeoSN users to control which information about them is available and to whom it is available. Thus, the lack of means to protect users privacy scares people bothered about privacy issues. This paper addresses a particular privacy threats that occur in GeoSNs: the Co-location privacy threat. It concerns the availability of information about the presence of multiple users in a same locations at given times, against their will. The challenge addressed is that of supporting privacy while still enabling useful services.
△ Less
Submitted 30 March, 2012; v1 submitted 18 March, 2012;
originally announced March 2012.
