4:30 - 5:00 |
Improving Software Through Automatic Untangling of Cyclic Dependencies
Cyclic dependencies among software components are considered an architectural problem that increases the development time and prevents proper reuse. One cause for the existence of such dependencies is the improper organization of elements into components.
Optimal reorganization of the components that resolves the cyclic dependencies in large and complex software systems is extremely difficult to perform manually and is not computationally feasible to perform automatically.
We present an approach for automatic untangling of cyclic dependencies among components for cycles of any size, having direct or transitive dependencies on one another. Our approach aims at minimizing the modifications to the original structure of the system, while taking into account various architectural properties.
We evaluate our solution on twelve open source and three industrial applications and demonstrate its applicability and value through architectural metrics and feedback from system architects. We evaluate our solution on twelve open source and three industrial applications, and demonstrate its applicability and value through architectural metrics and feedback from system architects.
|
|
Maayan Goldstein and Dany Moshkovich |
|
5:00 - 5:30 PM |
A Systematic Approach to Transforming System Requirements into Model Checking Specifications
In this paper, we propose a method that addresses the following dilemma: Model checking can formally expose Off-nominal behaviors (a major contributor to incompleteness in requirements), and unintended scenarios in the requirements of concurrent reactive systems. Requirements Engineers (RE) and those non-technical Stakeholders that are the system-to-be domain experts can greatly benefit from jointly using model checking during the elicitation, analysis, and verification of system-to-be requirements. However, model checking is a form of formal verification and many REs and domain experts typically lack the knowledge and training needed to apply model checking to the formal verification of requirements. There is a user gap between the advantages of model checking requirements and the ability to model check requirements. Our proposed method uses a Casual-Component Model to closes this gap, as we demonstrate using a real world application.
|
|
Daniel Aceituna, Hyunsook Do and Sudarshan Srinivasan |
|
5:30 - 6:00 PM |
A Candid Industrial Evaluation of Formal Software Verification using Model Checking
Model checking is a powerful formal analytical approach to verifying software and hardware systems. However, general industrial adoption is far from widespread. Some difficulties include the inaccessibility of techniques and tools and the need for further empirical evaluation in industrial contexts. This study considers the use of Simulink Design Verifier, a model checker that forms part of a modelling system already widely used in the safety-critical industry. Model checking is applied to a number of real-world problem reports, associated with aero-engine monitoring functions, to determine whether it can provide a practical route into effective verification, particularly for non-specialists. The study also considers the extent to which model checking can satisfy the requirements of the new airborne software assurance guidance DO-178C, which includes extensive guidance on formal methods. The study suggests that the benefits of model checking would be realised when it is targeted at parts of the software that are particularly error-prone, difficult to verify conventionally, or critical, in order to justify the effort of using and certifying the model checking techniques and tools.
|
|
Matthew Bennion and Ibrahim Habli |
|
6:00 - 6:30PM |
Architectural Dependency Analysis to Understand Rework Costs for Safety-Critical Systems
To minimize testing and technology upgrade costs for safety-critical systems, a thorough understanding and analysis of architectural dependencies is essential. Unmanaged dependencies create cost overruns and degraded qualities in systems. Architecture dependency analysis in practice, however, is typically performed in retrospect using code structures and/or the runtime image of a system. Retrospective analysis can miss important dependencies that surface earlier in the life cycle. Development artifacts such as the software architecture description and the software requirements specification can augment the analysis process; however, the quality, consistency, and content of these artifacts vary widely. It is therefore essential to identify architecture dependencies and to analyze them consistently throughout development. As a practical use case, we apply a commonly used dependency analysis metric, stability, and a visualization technique, the dependency structure matrix, to an architecture common to safety-critical systems that was re-engineered to reduce safety testing and technology upgrade cost. We highlight the gaps observed when running the analysis and discuss the need for early life-cycle dependency analysis for managing rework costs in industrial software development environments.
|
|
Robert Nord, Ipek Ozkaya, Raghvinder Sangwan and Ronald Koontz |
|