Validation and Verification Using Spatial Logic Framework for Building Layouts By Abhinav Fatehpuria Vineet Gupta 12 6 2005 ENPM 643 System Validation Verification 1 Agenda Background Spatial Logic 12 6 2005 Project Description Floor Plan Goals System Requirements System Structure Overview Application to Building Layouts Conclusion Software Used References ENPM 643 System Validation Verification 2 Background 12 6 2005 ENPM 643 System Validation Verification 3 Background Project Description Defined and categorized the design requirements of a building from an architectural view point Prepared the system structure Class Diagram at a higher level of abstraction Defined Validation Parameters To allow the architect to check potential building designs against the specification 12 6 2005 Quickly Easily In early phases of the design ENPM 643 System Validation Verification 4 Background Floor Plan F lo o r P la n Vent R e s tR o o m P assage W ay K itc h e n Window Joint B e d ro o m L iv in g R o o m Window O f f ic e 3 8 4 0 s q ft Window 12 6 2005 Window ENPM 643 System Validation Verification 5 Background Goals Cont d 12 6 2005 ENPM 643 System Validation Verification 6 Background System Requirements Architectural requirements of one bedroom apartment can be broadly categorized as Apartment Level 1 2 3 Room Level 4 5 6 7 8 12 6 2005 Area of the apartment should be at least 10000 sq units The apartment should have 1 bedroom 1 living room 1 kitchen 1 restroom and one passageway The apartment should have easy access to exit in case of fire Occupancy of the bedroom should be two Bedroom should be adjacent to the restroom Proximity strength between restroom and bedroom is 1 Bedroom should have air tight and sound proof doors Orientation of the bedroom should be towards the west ENPM 643 System Validation Verification 7 Background System Requirements 12 6 2005 ENPM 643 System Validation Verification 8 Background System Structure The complete architectural viewpoint is divided in to three sub classes Relationship Spaces Dividers Portals between different rooms Association Rooms between rooms and walls Association Rooms Walls between walls and portals Association Walls Portals The properties of these association classes 12 6 2005 Proximity strength address the proximity issue between different rooms Access Type What type of access is available Access Vent Is it for ventilation purpose Access Light Is it allowing light to pass through i e is it transparent Access admit Is it allowing people to enter or exit ENPM 643 System Validation Verification 9 Background System Structure G e n e ric C la s s D ia g ra m b in d A rc h ite c tu re S tr u c tu ra l P lu m b in g E le c tric ity V ie w P o in ts 1 1 A s s o c ia tio n W a lls P o rta ls Spaces D iv id e rs L e n g th B re a d th S h a p e 1 A s s o c ia tio n R o o m W a lls 1 N u m b e r o f W a lls P o rta ls In n e r O u te r A c c e s s V e n t A c c e s s L ig h t A c c e s s A d m it A c c e s s A u d ib le N o o f P o rta ls L e n g th B re a d th B a s e D is ta n c e Room s F lo o r L e n g th B re a d th H e ig h t O c c u p a n c y O rie n ta tio n 1 1 W a lls T h ic k n e s s In n e r o u te r B e d ro o m Passage W ay L iv in g ro o m J o in ts D o o rs A s s o c ia tio n R o o m s R e s tro o m 12 6 2005 K itc h e n P ro x im ity S tre n g th A c c e s s V e n t A c c e s s L ig h t A c c e s s A d m it A c c e s s A u d ib le ENPM 643 System Validation Verification W in d o w s Vent 10 Spatial Logic Its Application 12 6 2005 ENPM 643 System Validation Verification 11 Concept of Hyperplanes A conceptual border that divides two sets of points Each half forms a halfplane Mathematically it can be represented as l U 12 6 2005 ENPM 643 System Validation Verification 12 Half planes Represents spaces symbolically without any reference to a particular coordinate system The predicate hp x is a general representation of a halfplane according to its truth value E g hp a a 12 6 2005 ENPM 643 System Validation Verification 13 Halfplanes U p x y U always can be divided into exactly two subsets A and B defined by A p x y f x y 0 and B p x y f x y 0 f x y is a continuous function in U A and B are non empty closed sets Therefore A and B have the following characteristics A B is and U A U B is U A B 12 6 2005 ENPM 643 System Validation Verification 14 Defining Regions using Halfplanes 1 Given n halfplanes a region R is defined by a conjunctive formula of n hp x as R is hp a1 hp a2 hp an Since each halfplane can have truth value True or False each region is an interpretation of the Formula above For our floor plan U hp hp hp hp 12 6 2005 ENPM 643 System Validation Verification 15 Constraints hp b hp c hp c hp b hp b hp a hp b hp a 12 6 2005 ENPM 643 System Validation Verification 16 Defining Regions using Halfplanes 2 hp hp b hp a hp hp b hp hp c hp hp d U a R1 1 2 b c R5 R4 3 R2 R3 12 6 2005 4 ENPM 643 System Validation Verification 17 Restroom R1 hp a hp b hp d hp c hp a hp d Rest Room hp a a hp a b hp d hp d 12 6 2005 ENPM 643 System Validation Verification 18 Bedroom R2 hp a hp b hp d hp c hp b hp d Bed Room hp b b hp b hp d hp d 12 6 2005 ENPM 643 System Validation Verification 19 Living room R3 hp a hp b hp d hp b hp d Living Room b hp d hp d hp b …