Abstract
Achievement of quality in software design, while never easy, is made more difficult by the inherent complexity of hard real-time (HRT) design. Furthermore, timing requirements in HRT are by nature functional requirements, since system correctness depends on their fulfillment. Whereas the correctness dependence of the time imposes considering timing requirements from the early stages of the production process, complexity enforces a lifecycle model which fits in with requirements change and splits complexity by means of an incremental and iterative structure. Taking these aims as a starting point, this paper introduces SCTL/MUS-T methodology as supporting HRT design in a formalized and incremental way.