400
■
Handbook on Mobile and Ubiquitous Computing: Status and Perspective
or she can have mobile and ubiquitous control access to EGSMUC. The master can grant entry
access to the guest user irrespective of how he or she is connected to EGSMUC (mobile access) and
also irrespective of where he or she is located (ubiquitous access). We will model EGSMUC and
VERTAF will automatically synthesize and verify the code for the system.
16.3.1 UML Modeling
UML [23] is one of the most popular modeling and design languages in the industry. It standardizes
the diagrams and symbols used to build a system model. After scrutiny of all diagrams in UML,
we have chosen three diagrams for a user to input as system specification models, namely, class
diagram, sequence diagram, ...