Control Systems and Applications

Distributed Systems

Information Systems Security 1

Mgmt Measurement and Quality Cont

S Formal Methods for Software Eng

Software Arch and Design I

Software Arch and Design II

Software Process

Software Req and Specs

Software Test Verification and Qua

System Hardware Lab

User Interface Design

Web Based Enterprise App Design

Web Programming

SOEN331: Introduction to Formal Methods for Software Engineering Case study: Aircraft cabin pressurization system Dr. C. Constantinides November 21, 2014 1 Introduction Your assignment is to work in pairs and produce a formal speciﬁcation and a state diagram for a cabin pressurization system used in aircrafts and subsequently transform the two for- malisms into a declarative representation that you will extend with the deﬁnition of rules. You will execute queries to demonstrate the behavior of the system. 2 Background The following background 1 is taken from SKYbrary 2 , an electronic repository of information about navigation safety: Air pressure reduces with increase in altitude and therefore the amount of oxygen in any given volume of air also reduces with increase in altitude. Furthermore, the reduction in pressure impedes the ability of oxygen to pass across lung tissues and into the human blood- stream. The condition whereby the concentration of useful oxygen in the bloodstream is reduced because of a decrease in atmospheric pressure is known as Hypoxia 3 . In order to be able to ﬂy at high attitudes, the aircraft needs to be pressurised so that the crew and passengers can breathe without the need for supplemental oxygen. The cabin is contained within a sealed unit which is capable of containing air under pressure higher than the ambient pressure outside of the aircraft. Bleed air in gas turbine engines is compressed air that can be taken from within the engine. Bleed air from the aircraft’s engines is used to pressurize the cabin and air is released from 1 http://www.skybrary.aero/index.php/Aircraft Pressurisation Systems 2 http://www.skybrary.aero/index.php/Main Page 3 http://www.skybrary.aero/index.php/Hypoxia 1 the cabin by an outﬂow valve in order to prevent the cabin pressure from exceeding the maximum diﬀerential pressure. By using a cabin pressure regulator to manage the ﬂow of air through the outﬂow valve, the pressure within the aircraft can be increased or decreased as required, either to maintain a set cabin altitude or a set diﬀerential pressure . Cabin altitude is deﬁned as the cabin pressure expressed as an equivalent altitude above sea level and it is normally maintained at 2,400m as a compromise between the physiological needs of the crew and passengers and the structural limitations of the aircraft. At 2,400m the use of supplemental oxygen is not required. Diﬀerential pressure is deﬁned as the diﬀerence between cabin pressure and atmospheric pressure and must not exceed the maximum for which the aircraft is designed. As an aircraft climbs, for the comfort of the passengers, the pressurization system will grad- ually increase the cabin altitude and the diﬀerential pressure at the same time. A safety valve exists that can allow air into the cabin when the ambient pressure exceeds the cabin pressure. 3 Description of the system The system is initially idle. One would issue an activation signal and provided the engine is on, the system will become active. In becoming active, the system releases bleed air into the cabin while at the same time sets the range for Δ P MAX (the range of maximum diﬀerential pressure), and Δ P DESIRED which must be within Δ P MAX . When active, the system may receive a deactivation signal and become idle again. In becoming idle, the system stops bleeding air into the cabin. The system can only be shut oﬀ when idle. When becoming active, the system will immediately get into a normal mode. If at any time the system receives a signal indicating that the cabin has decompressed, the system will go into emergency mode while at the same time open the safety valve to maximum to allow air in, and perform an emergency descent. It will also deploy oxygen masks and sound an alarm. The system can only get back to normal mode if Δ P is within Δ P DESIRED and it doing so it will close the safety valve. When under normal operation, the system performs a cycle of readings and actions in order to increase or increase the pressure if and when required. The cycle starts with a coordinat- ing mode where the system will wait for 10 seconds and subsequently get into a regulating mode while at the same time perform certain readings that are vital for its proper opera- tion, namely the current cabin pressure and the current aircraft altitude. The system will also calculate the ambient pressure as a function of the current aircraft altitute and ﬁnally compute Δ P as the diﬀerence of the current cabin pressure and the ambient pressure. 2

SOEN | 331 | S Formal Methods for Software Eng | lecture notes | SOEN331: Introduction to Forma

Assertions Dr. C. Constantinides Department of Computer Science and Software Engineering Concordia University Montreal, Canada November 21, 2014 1 / 32 Programming with assertions  Deﬁnition: An assertion is a declarative statement that aﬃrms that a certain premise is true.  In a computer program, an assertion is a predicate that is assumed to be true. If found false, the assumption made by the assertion does not hold. 2 / 32 Programming with assertions /cont.  Prior to the execution of any modular unit, there is a condition on the expected state of the computation. This may for example be the type of the arguments passed to the module. This condition is referred to as the precondition of the module.  Furthermore, the successful termination of the module will change the state of the computation.  The expected new state is referred to as the postcondition of the module.  We can express this by the triple { P } S { Q } where S denotes the routine, P denotes the precondition and Q denotes the postcondition. P and Q are the module’s assertions. 3 / 32 Programming with assertions /cont.  If no precondition is imposed, we write true S { Q } Clients of the routine have the obligation to uphold the precondition. The routine has the obligation to uphold the postcondition upon successful termination. 4 / 32 Example: Factorial  Function factorial : N 0 → N 1 is deﬁned for non-negative integers by two guarded expressions as follows: factorial ( n )=  1 if n =0 n × factorial ( n - 1) if n > 0 5 / 32 Example: Factorial /cont.  For a routine S that computes this function, we can deﬁne the following triple: { n ∈ N ≥ 0 } S { S ( n )=Π n i =1 ( i ) if n > 0 , else 1 } where the precondition states that the input parameter must be a non-negative integer and the postcondition states that the return value of the routine must be the product of n × n - 1 × ... × 1 in the case that n > 0, and it must be 1 otherwise. 6 / 32 Example: Sum of ﬁrst n natural numbers  The sum of the ﬁrst n natural numbers is given by n  i =1 ( i )=1+2+3+ ... + n = n ( n + 1) 2 For a routine S that computes this function, we can deﬁne the following triple: { n ∈ N ≥ 1 } S { S ( n )= n  i =1 ( i ) } where the precondition states that the input parameter n must be a positive integer and the postcondition states that the return value of the routine must be the sum of 1 + 2 + ... + n . 7 / 32 Example: The sum of the ﬁrst n odd natural numbers  The sum of the ﬁrst n odd natural numbers is given by n  i =1 (2 i - 1) = 1 + 3 + 5 + ... + (2 n - 1) = n 2 For a routine S that computes this function, we can deﬁne the following triple: { n ∈ N ≥ 1 } S { S ( n )= n 2 } where the precondition states that the input parameter n must be a positive integer and the postcondition states that the return value of the routine must be n 2 . 8 / 32

SOEN | 331 | S Formal Methods for Software Eng | lecture notes | Assertions Dr. C. Constantinid

Information Systems Security (SOEN321) A Brief introduction to number Theory Dr. Amr Youssef Concordia Institute for Information Systems Engineering (CIISE) Concordia University Montreal, Canada youssef@ciise.concordia.ca Why do we need to learn number theory Many public key systems are based on number theoretic ideas Examples include  RSA (based on the difficulty of factoring)  Diffie-Hellman (based on the difficulty of solving the discrete log problem)  El-Gamal (based on discrete log)  etc. We will no dive deep into number theory. We will only learn what is necessary to understand these systems Modular Arithmetic Definition: a mod n = r  ∃ q s.t. a=q x n + r, where 0 ≤r ≤n -1 Example:  7 mod 3 = 1  -7 mod 3 = 2 Definition (Congruence) Groups Definition: A group ( G , *) is a set G on which a binary operation * is defined which satisfies the following axioms:  Closure: For all a , b Є G , a * b Є G  Associative: For all a , b , c Є G , (a * b)* c = a * (b * c)  Identity: ∃ e Є G s.t. for all a Є G , a* e = a = e * a  Inverse: For all a Є G, ∃ a -1 Є G s. t. a* a -1 = a -1 *a = e Example ( Z n , + ), where  Z n = {0, 1, ... , n - 1},  a + b = a + b mod n ( Z p * , × ), where  Z p * = {1, ... , p - 1}  a × b = a × b mod p Abelian Group  A group ( G , *) is called an abelian group if * is a commutative operation:  Commutative: For all a , b Є G , a * b = b * a . More explicit Example: (Z 7 ,+)  elements: {0,1,2,3,4,5,6}  5+4=2  0 is identity element  every element x has an inverse y such that x + y =0, what is the inverse of 3?  3+4=0, thus the inverse of 3 is 4. Example: (Z 7 ,×)  elements: (1,2,3,4,5,6)  what is the identity element?  what is the inverse of 3?  3×1=3, 3×2=6, 3×3=2, 3×4=5, 3×5=1, 3×6=4 Fields a fields F is a commutative ring in which all non -zero elements have multiplicative inverses Finite fields: if F contains a finite number of elements  the order must be of type p m with m>=1  for every order p m there is a unique (up to isomorphism) GF(p m ) Example:The field: Fp=(Z p ,+, ×) Example: F 7  solve 3 x +1=6  3 x = 5  x = 3 -1 ×5 = 5×5=4 Useful tools Extended Euclidian Algorithm Euclid’s Theorem Chinese reminder theorem Euclidian Algorithm Towards Extended Euclidian Algorithm Theorem: Given integers a, b > 0 and a > b, then d = gcd(a,b) is the least positive integer that can be represented as ax + by, x, y integer numbers. Corollary: if a and b are relative prime, then there exist x and y such that ax + by = 1. In other words, ax mod b = 1. How to find such x and y? Example Another example Example: determine gcd(803; 121) Solution

SOEN | 321 | Information Systems Security 1 | lecture notes | Information Systems Security (

Catalog of Refactorings  Name  common vocabulary  Summary  Motivation  When it should and should not be done  Code smells  Mechanics – step-by-step description  Simple example Pull Up Method (322) Motivation and When  Code Smells: duplicated code  Eliminate duplicate behavior  Often comes after other refactorings  e.g., extract method  If it depends on methods/fields in subclass, you may have to pull up other methods Mechanics  Ensure methods are identical  Change signature so they are the same  Create new method in superclass and copy method  Delete one subclass method  Compile and test  Keep deleting until only superclass  Possibly change callers to superclass Notes If your refactoring is easy make sure you discuss related refactorings and write some code to show how the refactoring works

SOEN | 343 | Software Arch and Design I | lecture notes | Catalog of Refactorings  Name

SRS-inspection-exercise.pdf

All courses in SOEN

Popular Documents