In this paper, we present formal semantics of UML (Unified Modeling Language) 
sequence diagrams using the PVS (Prototype Verification System) as an underlying 
semantic foundation. We give a formal definition of a trace-based semantics of UML
sequence diagrams; i.e. a sequence diagram is interpreted as a set of traces of 
events that may occur in the realization of the interaction specified by the 
sequence diagram. This work is a part of a long-term vision to explore how the PVS
tool set could be used to underpin practical tools for analysis of models in UML.
It also contributes to the ongoing effort to provide formal semantics of UML, 
with the aim of clarifying and disambiguating the language as well as supporting 
the development of semantically based tools.