CMPS 282 Final, Spring 2008

CMPS 282: Software Engineering II Instructor: Paul C. Attie Department of Computer Science American University of Beirut Problem Set 2 Due: Tuesday April 10 1 (10 points). Consider the following requirement R for a lift system: “if there are no customers inside the lift, then all outstanding panel button requests are cancelled” State this requirement in formal logic. Use the data model for the lift erxample given in class as a reference for introducing any needed data items, e.g, for outstanding requests. State the domain properties D and specification properties S that are needed to ensure that R is satisfied, and argue that D, S ⊢ R does in fact hold. 2 (15 points). Write a Buchi automaton for the requirement: “if the lift is at floor f and is moving up, and a panel button for floor f ′, where f ′ > f, is pressed, then the lift satisfies this request before changing direction” Is this property a pure safety property, a pure liveness property, or a combination of a safety and liveness property. Give an argument to support your answer. In case your answer is a combination of safety and liveness, give the Buich automata that express the pure safety and pure liveness parts of the property. 1