Nowadays the software systems, including web portals, are developed from a priori assumptions about how the system will be used. However, frequently these assumptions hold only partly and are defined also partially. Therefore one must be capable to compare the a priori assumptions with the actual user behavior in order to decide how the system could be improved. To tackle this problem, we consider a promising approach to employ the same formalism to express the intended usage, the web portal model and the frequent real usage patterns, extracted from the experimental data by data mining algorithms. This allows to automate the verification whether the frequent real usage patterns satisfy the intended usage in the web portal model. We propose to use temporal logic and Kripke structure as such a common formalism. Key words: Intended Usage, Real Usage, web Portal Model, Linear Temporal Logic, Pattern Mining