عنوان
پدید آورنده
موضوع
رده
کتابخانه
محل استقرار
شماره کتابشناسی ملی
شماره
TL52673
زبان اثر
زبان متن نوشتاري يا گفتاري و مانند آن
انگلیسی
عنوان و نام پديدآور
عنوان اصلي
Synthesis of Specifications and Refinement Maps for Real-time Object Code Verification
نام عام مواد
[Thesis]
نام نخستين پديدآور
Al-Qtiemat, Eman Mohammad
نام ساير پديدآوران
Srinivasan, Sudarshan K.
وضعیت نشر و پخش و غیره
نام ناشر، پخش کننده و غيره
North Dakota State University
تاریخ نشرو بخش و غیره
2020
يادداشت کلی
متن يادداشت
113 p.
یادداشتهای مربوط به پایان نامه ها
جزئيات پايان نامه و نوع درجه آن
Ph.D.
کسي که مدرک را اعطا کرده
North Dakota State University
امتياز متن
2020
یادداشتهای مربوط به خلاصه یا چکیده
متن يادداشت
Formal verification methods have been shown to be very effective in finding corner-case bugs and ensuring the safety of embedded software systems. The use of formal verification requires a specification, which is typically a high-level mathematical model that defines the correct behavior of the system to be verified. However, embedded software requirements are typically described in natural language. Transforming these requirements into formal specifications is currently a big gap. While there is some work in this area, we proposed solutions to address this gap in the context of refinement-based verification, a class of formal methods that have shown to be effective for embedded object code verification. The proposed approach also addresses both functional and timing requirements and has been demonstrated in the context of safety requirements for software control of infusion pumps. The next step in the verification process is to develop the refinement map, which is a mapping function that can relate an implementation state (in this context, the state of the object code program to be verified) with the specification state. Actually, constructing refinement maps often requires deep understanding and intuitions about the specification and implementation, it is shown very difficult to construct refinement maps manually. To go over this obstacle, the construction of refinement maps should be automated. As a first step toward the automation process, we manually developed refinement maps for various safety properties concerning the software control operation of infusion pumps. In addition, we identified possible generic templates for the construction of refinement maps. Recently, synthesizing procedures of refinement maps for functional and timing specifications are proposed. The proposed work develops a process that significantly increases the automation in the generation of these refinement maps. The refinement maps can then be used for refinement-based verification. This automation procedure has been successfully applied on the transformed safety requirements in the first part of our work. This approach is based on the identified generic refinement map templates which can be increased in the future as the application required.
اصطلاحهای موضوعی کنترل نشده
اصطلاح موضوعی
Computer engineering
اصطلاح موضوعی
Computer science
اصطلاح موضوعی
Electrical engineering
نام شخص به منزله سر شناسه - (مسئولیت معنوی درجه اول )
مستند نام اشخاص تاييد نشده
Al-Qtiemat, Eman Mohammad
نام شخص - ( مسئولیت معنوی درجه دوم )
مستند نام اشخاص تاييد نشده
Srinivasan, Sudarshan K.
شناسه افزوده (تنالگان)
مستند نام تنالگان تاييد نشده
North Dakota State University
دسترسی و محل الکترونیکی
نام الکترونيکي
مطالعه متن کتاب وضعیت انتشار
فرمت انتشار
p
اطلاعات رکورد کتابشناسی
نوع ماده
[Thesis]
کد کاربرگه
276903
اطلاعات دسترسی رکورد
سطح دسترسي
a
تكميل شده
Y
