ترغب بنشر مسار تعليمي؟ اضغط هنا

Towards Assurance-Driven Architectural Decomposition of Software Systems

290   0   0.0 ( 0 )
 نشر من قبل Ramy Shahin
 تاريخ النشر 2021
  مجال البحث الهندسة المعلوماتية
والبحث باللغة English
 تأليف Ramy Shahin




اسأل ChatGPT حول البحث

Computer systems are so complex, so they are usually designed and analyzed in terms of layers of abstraction. Complexity is still a challenge facing logical reasoning tools that are used to find software design flaws and implementation bugs. Abstraction is also a common technique for scaling those tools to more complex systems. However, the abstractions used in the design phase of systems are in many cases different from those used for assurance. In this paper we argue that different software quality assurance techniques operate on different aspects of software systems. To facilitate assurance, and for a smooth integration of assurance tools into the Software Development Lifecycle (SDLC), we present a 4-dimensional meta-architecture that separates computational, coordination, and stateful software artifacts early on in the design stage. We enumerate some of the design and assurance challenges that can be addressed by this meta-architecture, and demonstrate it on the high-level design of a simple file system.



قيم البحث

اقرأ أيضاً

In this work, we outline a cross-domain assurance process for safety-relevant software in embedded systems. This process aims to be applied in various different application domains and in conjunction with any development methodology. With this approa ch we plan to reduce the growing effort for safety assessment in embedded systems by reusing safety analysis techniques and tools for the product development in different domains.
115 - Radu Calinescu 2017
Building on concepts drawn from control theory, self-adaptive software handles environmental and internal uncertainties by dynamically adjusting its architecture and parameters in response to events such as workload changes and component failures. Se lf-adaptive software is increasingly expected to meet strict functional and non-functional requirements in applications from areas as diverse as manufacturing, healthcare and finance. To address this need, we introduce a methodology for the systematic ENgineering of TRUstworthy Self-adaptive sofTware (ENTRUST). ENTRUST uses a combination of (1) design-time and runtime modelling and verification, and (2) industry-adopted assurance processes to develop trustworthy self-adaptive software and assurance cases arguing the suitability of the software for its intended application. To evaluate the effectiveness of our methodology, we present a tool-supported instance of ENTRUST and its use to develop proof-of-concept self-adaptive software for embedded and service-based systems from the oceanic monitoring and e-finance domains, respectively. The experimental results show that ENTRUST can be used to engineer self-adaptive software systems in different application domains and to generate dynamic assurance cases for these systems.
Software architectural changes involve more than one module or component and are complex to analyze compared to local code changes. Development teams aiming to review architectural aspects (design) of a change commit consider many essential scenarios such as access rules and restrictions on usage of program entities across modules. Moreover, design review is essential when proper architectural formulations are paramount for developing and deploying a system. Untangling architectural changes, recovering semantic design, and producing design notes are the crucial tasks of the design review process. To support these tasks, we construct a lightweight tool [4] that can detect and decompose semantic slices of a commit containing architectural instances. A semantic slice consists of a description of relational information of involved modules, their classes, methods and connected modules in a change instance, which is easy to understand to a reviewer. We extract various directory and naming structures (DANS) properties from the source code for developing our tool. Utilizing the DANS properties, our tool first detects architectural change instances based on our defined metric and then decomposes the slices (based on string processing). Our preliminary investigation with ten open-source projects (developed in Java and Kotlin) reveals that the DANS properties produce highly reliable precision and recall (93-100%) for detecting and generating architectural slices. Our proposed tool will serve as the preliminary approach for the semantic design recovery and design summary generation for the project releases.
519 - Ramy Shahin 2021
In this paper we introduce the notion of Modal Software Engineering: automatically turning sequential, deterministic programs into semantically equivalent programs efficiently operating on inputs coming from multiple overlapping worlds. We are drawin g an analogy between modal logics, and software application domains where multiple sets of inputs (multiple worlds) need to be processed efficiently. Typically those sets highly overlap, so processing them independently would involve a lot of redundancy, resulting in lower performance, and in many cases intractability. Three application domains are presented: reasoning about feature-based variability of Software Product Lines (SPLs), probabilistic programming, and approximate programming.
Safety-critical software systems are in many cases designed and implemented as families of products, usually referred to as Software Product Lines (SPLs). Products within an SPL vary from each other in terms of which features they include. Applying e xisting analysis techniques to SPLs and their safety cases is usually challenging because of the potentially exponential number of products with respect to the number of supported features. In this paper, we present a methodology and infrastructure for certified emph{lifting} of existing single-product safety analyses to product lines. To ensure certified safety of our infrastructure, we implement it in an interactive theorem prover, including formal definitions, lemmas, correctness criteria theorems, and proofs. We apply this infrastructure to formalize and lift a Change Impact Assessment (CIA) algorithm. We present a formal definition of the lifted algorithm, outline its correctness proof (with the full machine-checked proof available online), and discuss its implementation within a model management framework.
التعليقات
جاري جلب التعليقات جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا