Application software in pervasive computing is required to control devices embedded in the environment by being aware of the contexts on which effectiveness of the devices depend. Developers face difficulties to enumerate involved physical prerequisites for effective use of devices and undesirable situations to be avoided, as well as define consistent behaviors of the application software. This study provides a theoretical framework for formal modeling of requirements, assumptions and behaviors for application software in pervasive computing. This study specifically focuses on prerequisites for physical (visual, audio, etc.) interactions, which are defined and examined in terms of scopes and their relationships not limited to tree structures. This study also explores analysis and verification based on the formal modeling, using of an existing reasoner.