This talk gives an overview of the safety analysis performed for NASA's Small Aircraft Transportation System, Higher Volume Operations (SATS-HVO) Concept of Operations. The analysis is based on the set of rules that governs the entry and operation inside a Self Controlled Airspace (SCA). In the SCA, aircraft flying under instrument flight rules maintain separation using the concept rules and on-board avionic tools, without Air Traffic Control services. A mathematical model of the concept of operation is used to verify the safety properties. The verification is performed using an explicit state exploration algorithm written and proven correct in PVS (Prototype Verification System).