본 논문은 SCR 방법으로 작성된 요구사항 명세의 정형적인 의미론을 제안한다. 먼저 우리는 SCR 명세를 시간적전이시스템으로 변환함으로써 SCR 명세의 의미론을 정의한다. 그리고 우리는 SCR 방법을 실시간 시스템의 명세를 위하여 확장하며, 확장된 SCR 명세의 의미론 또한 시간적전이시스템으로의 변환을 통하여 정의한다. 이러한 의미론은 SCR 명세의 병행성과 시간 개념을 제대로 나타낼 수 있으며, 시간적전이시스템에서의 검증 방법을 SCR 명세의 검증에 직접 적용할 수 있게 하는 장점이 있다.Abstract This paper presents a formal semantics for requirements specifications written in the SCR method. We define a semantics for SCR specifications by a translational approach into timed transition systems. Then we extend the SCR method for real-time systems and define a semantics for timed SCR specifications. The main benefit from providing such semantics is that it provides a natural modeling of concurrency and time in SCR specifications. The semantics enables us to directly apply verification methods for timed transition systems to SCR specifications.