Abstract: The paper discusses a methodology for capturing, representing, and analyzing software requirements specification of real time, autonomous systems. Temporal requirements and constraints often make it difficult to fully capture and analyze the behavior of entities of real time, autonomous systems at the abstract level and early in the software development process. If high level domain knowledge and the expected functionalities of the system are specified using first order logic (and/or temporal logic), the resultant specification would provide a sound, logical basis for further analysis and verification early in the life cycle. Formal methods and tools (e.g., propositional and predicate calculus) as well as theorem proving procedures, together, provide a viable methodological solution to the problem.