CMPS 282 Final, Spring 2008

CMPS 282: Software Engineering II Instructor: Paul C. Attie Department of Computer Science American University of Beirut Problem Set 1 Due: Thursday March 15 In all your answers, you may extend the given examples as needed to answer the question properly. 1 (5 points). Write the following statement in first order logic: In every company, there is exactly one employee who has no manager. 2 (5 points). Give a Buchi automaton that accepts the following required property for the single customer banking example: Every request(a, m) operation is followed by either a payout(a′, m) operation or by a reject(a′′, m) operation. Be sure to give an appropriate designation for reject(a′′, m) 3 (5 points). Give a Buchi automaton that accepts the following required property for the single customer banking example: Every request(a, m) operation is followed by a matching payout(a′, m) operation if the account balance is greater than or equal to m at the time that request(a, m) is executed. 4 (10 points). Modify the requirements statement for the banking example given in the lecture notes to add the concept of interest. Interest should be computed each month. Introduce all needed concepts and designate or define them as appropriate. Rewrite the domain property that defines the account balance in terms of the operations executed on the account. 5 (5 points). Give a Buchi automaton that accepts the following required property for a lift system: If the lift is at floor 1 and is traveling in the upwards direction, and there are outstanding up requests at floors 4 and 7, then the lift will stop at floor 4 before it stops at floor 7. 1