A formal approach to design and analysis of rule-based systems incorporated into embedded systems is presented in the paper. RTCP-nets, a subclass of timed coloured Petri nets, are used as a modelling language. They enable modeling of embedded systems incorporating an RBS (rule-based system). Such a system is represented as a D-net (decision net) that constitutes the bottom layer of the model. D-nets are used to represent a set of generalized decision rules with non-atomic attribute values. In order to assure reliable and efficient performance, analysis and verification of selected qualitative properties (such as completeness, consistency and optimality) are carried out. The analysis and verification stage are based on Petri nets analysis methods and are included into the design process. Design and verification are supported by computer tools.