Đang chuẩn bị liên kết để tải về tài liệu:
Lecture Formal methods in software engineering - Lecture 31

Không đóng trình duyệt đến khi xuất hiện nút TẢI XUỐNG Tải xuống

Lecture Formal methods in software engineering - Lecture 31: Applications of formal methods. This chapter presents the following content: A real application; testing based on formal methods; another real application; model construction and model checking beyond what you have seen in this entire set of lectures; a third, very real application; wrap up. | Formal Methods in Software Engineering Applications of Formal Methods Lecture 31 This Part We apply the concepts, methods and tools you learnt to love in contexts that are relatively close to what the people out there are facing. In this lecture I show you what they are facing, and I round off the entire lecture series. Assumptions for today: Nothing particular. Contents of this lecture A real application. Testing based on formal methods. Another real application. Model construction and model checking beyond what you have seen in this entire set of lectures. A third, very real application. Wrap up. What’s this? Nieuwe Waterweg Storm surge barrier North Sea Rotterdam First planned in 1953. Completed in 1999. Some statistical data: Each barrier wall has the height of one Eifel Tour, and weighs twice as much. Decision are taken 24 hrs before actual closure, Reversible until 3 hrs before closure. Fully mechanised -software controlled - decision procedure. Nieuwe Waterweg Storm surge barrier (where ‘fully’ means FULLY’). Nieuwe Waterweg Storm surge barrier North Sea Rotterdam ‘BESW’ ‘BOS’ North Wall South Wall The Storm surge barrier System consists of distributed components: north wall, south wall, various hydraulic parts, engines, etc. BOS (‘beslissing & ondersteunend systeem’) knows the environmental conditions; takes decisions, based on the available data; BESW (‘besturingssysteem waterweg’) knows & controls the barrier; carries out commands of BOS; reports status information to BOS; The design philosophy taken from ‘Ministerie van Verkeer en Waterstaat’ ‘BBI’ (BOS-BESW Interface) The Storm surge barrier Budget issues Total costs > 500 million €; Costs for software The Storm surge . | Formal Methods in Software Engineering Applications of Formal Methods Lecture 31 This Part We apply the concepts, methods and tools you learnt to love in contexts that are relatively close to what the people out there are facing. In this lecture I show you what they are facing, and I round off the entire lecture series. Assumptions for today: Nothing particular. Contents of this lecture A real application. Testing based on formal methods. Another real application. Model construction and model checking beyond what you have seen in this entire set of lectures. A third, very real application. Wrap up. What’s this? Nieuwe Waterweg Storm surge barrier North Sea Rotterdam First planned in 1953. Completed in 1999. Some statistical data: Each barrier wall has the height of one Eifel Tour, and weighs twice as much. Decision are taken 24 hrs before actual closure, Reversible until 3 hrs before closure. Fully mechanised -software controlled - decision procedure. .