•A large amount of ROS packages ends up being abandoned by their developers.•ROS package reuse is not as easy as promised: bugs and lack of basic documentation hamper reuse.•Members of the ROS ...ecosystem do not contribute because they lack time or confidence in their possible contribution.•We can improve the ROS ecosystem by identifying and predicting abandoned packages.•Recommender systems can be used to propose contribution opportunities to community members.
ROS, the Robot Operating System, offers a core set of software for operating robots that can be extended by creating or using existing packages, making it possible to write robotic software that can be reused on different hardware platforms. With thousands of packages available per stable distribution, encapsulating algorithms, sensor drivers, etc., it is the de facto middleware for robotics. Like any software ecosystem, ROS must evolve in order to keep meeting the requirements of its users. In practice, packages may end up being abandoned between releases: no one may be available to update a package, or newer packages offer similar functionality. As such, we wanted to identify and understand the evolution challenges faced by the ROS ecosystem. In this article, we report our findings after interviewing 19 ROS developers in depth, followed by a focus group (4 participants) and an online survey of 119 ROS community members. We specifically focused on the issues surrounding package reuse and how to contribute to existing packages. To conclude, we discuss the implications of our findings, and propose five recommendations for overcoming the identified issues, with the goal of improving the health of the ROS ecosystem.
Affirmative action in college admissions has been touted as a way to close the gender gap in science, technology, engineering, and mathematics programs. We report a study of one such program, where ...we discovered a positive effect on female enrollment and a smaller effect on a combined computer science and software engineering degree.
Context: Software Product Lines (SPL) evolve when there are changes in the requirements, product structure or the technology being used. Different approaches have been proposed for managing SPL ...assets and some also address how evolution affects these assets. Existing mapping studies have focused on specific aspects of SPL evolution, but there is no cohesive body of work that gives an overview of the area as a whole.
Objective: The goals of this work are to review the characteristics of the approaches reported as supporting SPL evolution, and to synthesize the evidence provided by primary studies about the nature of their processes, as well as how they are reported and validated.
Method: We conducted a systematic literature review, considering six research questions formulated to evaluate evolution approaches for SPL. We considered journal, conference and workshop papers published up until March 2017 in leading digital libraries for computer science.
Results: After a thorough analysis of the papers retrieved from the digital libraries, we ended up with a set of 60 primary studies. Feature models are widely used to represent SPLs, so feature evolution is frequently addressed. Other assets are less frequently addressed. The area has matured over time: papers presenting more rigorous work are becoming more common. The processes used to support SPL evolution are systematic, but with a low level of automation.
Conclusions: Our research shows that there is no consensus about SPL formalization, what assets can evolve, nor how and when these evolve. Case studies are quite popular, but few industrial-sized case studies are publicly available. Also, few of the proposed techniques offer tool support. We believe that the SPL community needs to work together to improve the state of the art, creating methods and tools that support SPL evolution in a more comparable manner.
Web service applications are distributed processes that are composed of dynamically bounded services. In our previous work 15, we have described a framework for performing runtime monitoring of web ...service against behavioural correctness properties (described using property patterns and converted into finite state automata). These specify forbidden behavior (safety properties) and desired behavior (bounded liveness properties). Finite execution traces of web services described in BPEL are checked for conformance at runtime. When violations are discovered, our framework automatically proposes and ranks recovery plans which users can then select for execution. Such plans for safety violations essentially involve "going back" - compensating the executed actions until an alternative behaviour of the application is possible. For bounded liveness violations, recovery plans include both "going back" and "re-planning" - guiding the application towards a desired behaviour. Our experience, reported in 16, identified a drawback in this approach: we compute too many plans due to (a) overapproximating the number of program points where an alternative behaviour is possible and (b) generating recovery plans for bounded liveness properties which can potentially violate safety properties. In this paper, we describe improvements to our framework that remedy these problems and describe their effectiveness on a case study.
Web service applications are distributed processes that are composed of dynamically bounded services. In this paper, we give a definitive description of a framework for performing runtime monitoring ...of web service applications against behavioural correctness properties described as finite state automata. These properties specify forbidden and desired interactions between service partners. Finite execution traces of web service applications described in BPEL are checked for conformance at runtime. When violations are discovered, our framework automatically proposes adaptation strategies, in the form of plans, which users can select for execution. Our framework also allows verification of stated pre- and post-conditions of service partners and provides guarantees of correctness of the generated recovery plans.
Formal verification means to rigorously explore the correctness of system designs expressed as mathematical models, most likely with the assistance of modern computers. Original approaches were to ...model and express a distributed system using existing theoretical tools such as Petri Nets. Nevertheless the main problems of such approaches are the restrictions imposed by formal tools and the human factor of simplify and model a distributed system. We propose a way to do formal verification of a distributed system by modeling the communication of the system as a concurrent program, instantiating the distributed system using threads and atomic queues and testing/verifying directly to the source code with specialized verifiers for concurrent programs. As an example, we show the verification of a distributed threshold signer using CBMC verifying properties such as memory leaks, index out of bounds, and data races.
For a system of distributed processes, correctness can be ensured by (statically) checking whether their composition satisfies properties of interest. However, Web services are distributed processes ...that dynamically discover properties of other Web services. Since the overall system may not be available statically and since each business process is supposed to be relatively simple, we propose to use runtime monitoring of conversations between partners as a means of checking behavioral correctness of the entire Web service system. Specifically, we identify a subset of UML 2.0 sequence diagrams as a property specification language and show that it is sufficiently expressive for capturing safety and liveness properties. By transforming these diagrams to automata, we enable conformance checking of finite execution traces against the specification. We show how our language can be used to specify the specification property system (SPS). We describe an implementation of our approach as part of an industrial system. Finally, we discuss our experience of specifying and monitoring a number of properties from three existing applications.
MDE software process lines in small companies Hurtado, Julio Ariel; Bastarrica, María Cecilia; Ochoa, Sergio F. ...
The Journal of systems and software,
20/May , Volume:
86, Issue:
5
Journal Article
Peer reviewed
► We define an MDE approach for software process lines. ► We illustrate our approach with an academic example. ► We validate our approach in two different industrial settings. ► Reusing tailoring ...knowledge makes software process instantiation more reliable and repeatable. ► Software processes tailored to project context have the potential to be more productive and to yield better products.
Software organizations specify their software processes so that process knowledge can be systematically reused across projects. However, different projects may require different processes. Defining a separate process for each potential project context is expensive and error-prone, since these processes must simultaneously evolve in a consistent manner. Moreover, an organization cannot envision all possible project contexts in advance because several variables may be involved, and these may also be combined in different ways. This problem is even worse in small companies since they usually cannot afford to define more than one process. Software process lines are a specific type of software product lines, in the software process domain. A benefit of software process lines is that they allow software process customization with respect to a context. In this article we propose a model-driven approach for software process lines specification and configuration. The article also presents two industrial case studies carried out at two small Chilean software development companies. Both companies have benefited from applying our approach to their processes: new projects are now developed using custom processes, process knowledge is systematically reused, and the total time required to customize a process is much shorter than before.
When model-checking reports that a property holds on a model,
vacuity detection
increases user confidence in this result by checking that the property is satisfied in the intended way. While vacuity ...detection is effective, it is a relatively expensive technique requiring many additional model-checking runs. We address the problem of efficient vacuity detection for Bounded Model Checking (BMC) of linear temporal logic properties, presenting three partial vacuity detection methods based on the efficient analysis of the resolution proof produced by a successful BMC run. In particular, we define a characteristic of resolution proofs—
peripherality
—and prove that if a variable is a source of vacuity, then there exists a resolution proof in which this variable is peripheral. Our vacuity detection tool,
VaqTree
, uses these methods to detect vacuous variables, decreasing the total number of model-checking runs required to detect all sources of vacuity.
PDF
