A formal method for modeling and analysis of requirements for software /

Requirements that are well understood by a client and a provider are a major contributor to developing and supporting reliable, quality software on time and within budget. This thesis has two thrusts to facilitate improved interpretation of requirements: (1) a requirements model and (2) a new formalism called LaP, with automated tools, to express and analyze requirements. The new formalism is based on the integration of an algebraic based language, Larch, and an extended finite state machine based language, Promela. Larch comes with a theorem prover (Larch Prover) and Promela comes with a tool (SPIN) to aid in the validation of dynamic properties. It is the objective of LaP to express the control and data intensive aspects of requirements. The two thrusts are demonstrated by building a requirements model for real telecommunications requirements that ask for a system that can manage the access configurations of user's accounts in telecommunications equipment