اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدOn Formal Methods for Collective Adaptive System Engineering. {Scalable Approximated, Spatial} Analysis Techniques. Extended Abstract
365
0
0.0
(
0
)
تأليف
Diego Latella
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
In this extended abstract a view on the role of Formal Methods in System Engineering is briefly presented. Then two examples of useful analysis techniques based on solid mathematical theories are discussed as well as the software tools which have been built for supporting such techniques. The first technique is Scalable Approximated Population DTMC Model-checking. The second one is Spatial Model-checking for Closure Spaces. Both techniques have been developed in the context of the EU funded project QUANTICOL.
قيم البحث
اقرأ أيضاً
Collective Adaptive Systems (CAS) consist of a large number of spatially distributed heterogeneous entities with decentralised control and varying degrees of complex autonomous behaviour that may be competing for shared resources even when collaborat
ing to reach common goals. It is important to carry out thorough quantitative modelling and analysis and verification of their design to investigate all aspects of their behaviour before they are put into operation. This requires combinations of formal methods and applied mathematics which moreover scale to large-scale CAS. The primary goal of FORECAST is to raise awareness in the software engineering and formal methods communities of the particularities of CAS and the design and control problems which they bring.
Designing software that controls industrial equipment is challenging, especially due to its inherent concurrent nature. Testing this kind of event driven control software is difficult and, due to the large number of possible execution scenarios only
a low dynamic test coverage is achieved in practice. This in turn is undesirable due to the high cost of software failure for this type of equipment. In this paper we describe the Dezyne language and tooling; Dezyne is a programming language aimed at software engineers designing large industrial control software. We discuss its underlying two layered and compositional approach that enables reaping the benefits of Formal Methods, hereby strongly supporting guiding principles of software engineering. The core of Dezyne uses the mCRL2 language and model-checker (Jan Friso Groote et al.) to verify the correctness and completeness of all possible execution scenarios. The IDE of Dezyne is based on the Language Server Protocol allowing a smooth integration with e.g., Visual Studio Code, and Emacs, extended with several automatically generated interactive graphical views. We report on the introduction of Dezyne and its predecessor at several large high-tech equipment manufacturers resulting in a decrease of software developing time and a major decrease of reported field defects.
Trust and reputation models for distributed, collaborative systems have been studied and applied in several domains, in order to stimulate cooperation while preventing selfish and malicious behaviors. Nonetheless, such models have received less atten
tion in the process of specifying and analyzing formally the functionalities of the systems mentioned above. The objective of this paper is to define a process algebraic framework for the modeling of systems that use (i) trust and reputation to govern the interactions among nodes, and (ii) communication models characterized by a high level of adaptiveness and flexibility. Hence, we propose a formalism for verifying, through model checking techniques, the robustness of these systems with respect to the typical attacks conducted against webs of trust.
In the software development process, model transformation is increasingly assimilated. However, systems being developed with model transformation sometimes grow in size and become complex. Meanwhile, the performance of model transformation tends to d
ecrease. Hence, performance is an important quality of model transformation. According to current research model transformation performance focuses on optimising the engines internally. However, there exists no research activities to support transformation engineer to identify performance bottleneck in the transformation rules and hence, to predict the overall performance. In this paper we vision our aim at providing an approach of monitoring and profiling to identify the root cause of performance issues in the transformation rules and to predict the performance of model transformation. This will enable software engineers to systematically identify performance issues as well as predict the performance of model transformation.
This volume contains the proceedings of the First International Workshop of Formal Techniques for Safety-Critical Systems (FTSCS 2012), held in Kyoto on November 12, 2012, as a satellite event of the ICFEM conference. The aim of this workshop is to
bring together researchers and engineers interested in the application of (semi-)formal methods to improve the quality of safety-critical computer systems. FTSCS is particularly interested in industrial applications of formal methods. Topics include: - the use of formal methods for safety-critical and QoS-critical systems, including avionics, automotive, and medical systems; - methods, techniques and tools to support automated analysis, certification, debugging, etc.; - analysis methods that address the limitations of formal methods in industry; - formal analysis support for modeling languages used in industry, such as AADL, Ptolemy, SysML, SCADE, Modelica, etc.; and - code generation from validated models. The workshop received 25 submissions; 21 of these were regular papers and 4 were tool/work-in-progress/position papers. Each submission was reviewed by three referees; based on the reviews and extensive discussions, the program committee selected nine regular papers, which are included in this volume. Our program also included an invited talk by Ralf Huuck.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
