UMD ENSE 623 - Boarding Pass Issuance to Passengers at Airport

Unformatted text preview:

111ENSE623/ENPM645ENSE623/ENPM645By Soe ZarniBargava SubramanianUniversity of MarylandDecember 6, 2005Boarding Pass Issuance to Passengers at Airport222System Boundary DescriptionSystem Boundary DescriptionAirport authorities have fixed(constrained) space in airport which the airlines can use to set up counters to issue boarding pass. Passengers of various airlines come and wait in the space in theform of queue to obtain their boarding pass.Requirements :Airlines : Issue boarding pass to passengersPassenger : obtain boarding pass333Problem StatementProblem StatementA specific example :Fixed room area where three counters are set up.Two airlines operate.Each owns one counterThey share the third counter.variesCounter 1Counter 2 (Share)Counter 3Airline A Airline B444Our twoOur two--fold approachfold approachSolving Spatial Constraint•How do the airlines determine their operating space ? •How should their queue structure be ?Solving Temporal Constraint•Do the passengers catch the flight on time ? - we do not consider •Do the airlines process the passengers so that they catch the flight ?- Yes – but there is an assumption – to avoid complications – we assume that if airline obtain extra counter – they process the extra burden and are well-off.555Spatial ConstraintSpatial ConstraintAccomplish the following tasks :•Determine number of operating counters required at a specific time• Given operating space for the airlines, the queue length has to be determined.Both of the above problems are inherently the same.Procedure :1) Start each airline with just one counter and with just one queue line2) Check periodically the population of the queue.3) Whenever the queue becomes congested, add one more line4) When the whole counter space is nearing capacity, request for the next counter.5) Temporal logic provides solution of when next counter is made available.6) Reassign population amongst both the counters in a fair manner.7) Release counter when done or when requested.666Binary Space Partitioning TreeBinary Space Partitioning Tree•Binary space partitioning (BSP) is a method for recursively subdividing a space into convex sets by hyperplanes. •This subdivision gives rise to a representation of the scene by means of a tree data structure known as a BSP tree.“BSP tree construction is a process which takes a subspace and partitions it by any hyperplanethat intersects the interior of that subspace. The result is two new subspaces that can be further partitioned by recursive application of the method.““• Our problem is a BSP tree data-structure - variant.• A point is represented by a vector P(x,y,z)• A plane is represented by a vector (P,p). P is the normal vector to plane.Possible Extensions: Incorporate Quad-trees for queue formation. Quad-trees recursively divide given subspace into 4 subspaces.777Temporal Constraint Temporal Constraint --UPPAALUPPAAL• Temporal logic is validated using UPPAAL.“Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata”•• Model Each automaton• For each automaton, specify entry and exit conditions.• Two exit conditions – Guard and Invariant• Guard – exit condition based on an event happening at/within a particular time•Invariant – upperbound for the state – max.(or min.) time one spends on the state.•Syncronization – Trigger an event in another automaton on satisfaction of some constraint of this automaton.•Templates(or Events) communicate through edges – having constraints.888UPPAALUPPAAL• State Check :(i) Reachability – Can we reach from State A to State B ?(ii) Safety – Can two events occur simultaneously ?(iii) Liveness – if some event happens – does it trigger another event at some later point of time ?• UPPAAL has 3 screens :(i) System editor – where all timed automata and constriants are specified(ii) Simulator – Active transactions and the Message Sequence Chart is displayed – we can trace flow of any transaction(iii) Verifier – specify state check properties and see if it is satisfied.999Temporal LogicTemporal Logic“It took a lot of time to learn the tool – no simple walk-through example provided. Modeling time constraints is a bit tricky. We took quite a lot of time to understand the tool.”The UPPAAL system we modeled has the following features/constraints(i) The request for counter happens 30 min before actual counter taking over(ii) The other airline has 25 min to respond(iii) If no response for 25 min – the airline which made the request gets the counter(iv) Setting up of counter takes 5 min(v) Airline can have the counter for max of 90 min – after that it becomes empty – whoever requests it next gets it.(vi) Two airlines cannot simultaneously hold the counter(vii) More verifying properties – on the model – DEMO TIME !101010WorkWork--inin--Progress/Future StepsProgress/Future StepsCost Evaluation : We are currently writing simple optimization equations for the problem. We are considering only the airline perspectiveTo optimize :Minimize ExpenseWhere Expense is composed of :Operating Expense : No. of hours they use the extra counter counter – composed of materials and personnel used for the extra counterPassenger Reimbursement : Amount they need to pay the passenger when he misses the flightSubject to constraints :Passenger Arrival RateAverage Process timeAverage counter setting-up time111111WorkWork--InIn--Progress/Future Steps (Contd.)Progress/Future Steps (Contd.)Spatial Logic Model Checker:We are using the SLMC tool that allows the user to automatically verify behavioral and spatial properties of distributed concurrent systems to validate spatial logic for a simplified case Further details about tool : Further details about tool : http://ctp.di.fct.unl.pt/SLMC/More about Cost UPPAAL CORA is a branch of UPPAAL for Cost Optimal Reachability Analysis. Uses the timed automata LPTA.121212Thank You Dr. AustinThank You Dr.


View Full Document

UMD ENSE 623 - Boarding Pass Issuance to Passengers at Airport

Download Boarding Pass Issuance to Passengers at Airport
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Boarding Pass Issuance to Passengers at Airport and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Boarding Pass Issuance to Passengers at Airport 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?