A three-dimensional hierarchical concept of formal specifications’ abstraction level variation has been introduced. Specifications based on the formalism of the Temporal Logic of Actions have been approached as the design artifacts making it possible to conduct the model checking in an automated manner. Concept is grounded on conducting the stratification. It has been approached as an instrument allowing the developers of safety-critical software systems vary the abstraction level of formal specifications they use in accordance with available time and/or computational resources. Case study has been conducted grounding on the scenarios taking place in energy. To this end, spatial properties of corresponding specifications and related transition systems have been considered and estimated. Obtained experimental results have allowed to formulate an assumption regarding the expedience of concept usage by software developers to meet the effect of an exponential growth of the state space of transition system taking place during the process of automated model checking.