[{"abstract":[{"lang":"eng","text":"This article presents an approach, which combines theorem proving-based refinement with model checking for state based real-time systems. Our verification flow starts from UML state diagrams, which are translated to the formal B language and are model checked for real-time properties. By means of the B language and a B theorem prover, refined state diagrams are verified against their abstract representation. The approach is presented by means of the refinement of a digital echo cancellation unit."}],"citation":{"chicago":"Krupp, Alexander, Wolfgang Müller, and Ian Oliver. “Formal Refinement and Model Checking of An Echo Cancellation Unit.” In <i>Proceedings of DATE’04 Designers’ Forum</i>. Paris, 2004. <a href=\"https://doi.org/10.1109/DATE.2004.1269214\">https://doi.org/10.1109/DATE.2004.1269214</a>.","short":"A. Krupp, W. Müller, I. Oliver, in: Proceedings of DATE’04 Designers’ Forum, Paris, 2004.","apa":"Krupp, A., Müller, W., &#38; Oliver, I. (2004). Formal Refinement and Model Checking of An Echo Cancellation Unit. <i>Proceedings of DATE’04 Designers’ Forum</i>. Proceedings Design, Automation and Test in Europe Conference and Exhibition. <a href=\"https://doi.org/10.1109/DATE.2004.1269214\">https://doi.org/10.1109/DATE.2004.1269214</a>","ieee":"A. Krupp, W. Müller, and I. Oliver, “Formal Refinement and Model Checking of An Echo Cancellation Unit,” presented at the Proceedings Design, Automation and Test in Europe Conference and Exhibition, 2004, doi: <a href=\"https://doi.org/10.1109/DATE.2004.1269214\">10.1109/DATE.2004.1269214</a>.","ama":"Krupp A, Müller W, Oliver I. Formal Refinement and Model Checking of An Echo Cancellation Unit. In: <i>Proceedings of DATE’04 Designers’ Forum</i>. ; 2004. doi:<a href=\"https://doi.org/10.1109/DATE.2004.1269214\">10.1109/DATE.2004.1269214</a>","bibtex":"@inproceedings{Krupp_Müller_Oliver_2004, place={Paris}, title={Formal Refinement and Model Checking of An Echo Cancellation Unit}, DOI={<a href=\"https://doi.org/10.1109/DATE.2004.1269214\">10.1109/DATE.2004.1269214</a>}, booktitle={Proceedings of DATE’04 Designers’ Forum}, author={Krupp, Alexander and Müller, Wolfgang and Oliver, Ian}, year={2004} }","mla":"Krupp, Alexander, et al. “Formal Refinement and Model Checking of An Echo Cancellation Unit.” <i>Proceedings of DATE’04 Designers’ Forum</i>, 2004, doi:<a href=\"https://doi.org/10.1109/DATE.2004.1269214\">10.1109/DATE.2004.1269214</a>."},"publication":"Proceedings of DATE’04 Designers' Forum","department":[{"_id":"672"}],"keyword":["Echo cancellers","Logic","Unified modeling language","Automata","Data structures","Boolean functions","Electronic design automation and methodology","Prototypes","Specification languages","Constraint theory"],"type":"conference","place":"Paris","date_created":"2023-01-24T08:53:26Z","date_updated":"2023-01-24T08:53:31Z","conference":{"name":"Proceedings Design, Automation and Test in Europe Conference and Exhibition"},"publication_identifier":{"isbn":["0-7695-2085-5"]},"author":[{"full_name":"Krupp, Alexander","first_name":"Alexander","last_name":"Krupp"},{"id":"16243","last_name":"Müller","first_name":"Wolfgang","full_name":"Müller, Wolfgang"},{"full_name":"Oliver, Ian","first_name":"Ian","last_name":"Oliver"}],"title":"Formal Refinement and Model Checking of An Echo Cancellation Unit","year":"2004","status":"public","doi":"10.1109/DATE.2004.1269214","user_id":"5786","_id":"39061","language":[{"iso":"eng"}]},{"citation":{"ama":"Haeb-Umbach R. Automatic generation of phonetic regression class trees for MLLR adaptation. <i>IEEE Transactions on Speech and Audio Processing</i>. 2001;9(3):299-302. doi:<a href=\"https://doi.org/10.1109/89.906003\">10.1109/89.906003</a>","bibtex":"@article{Haeb-Umbach_2001, title={Automatic generation of phonetic regression class trees for MLLR adaptation}, volume={9}, DOI={<a href=\"https://doi.org/10.1109/89.906003\">10.1109/89.906003</a>}, number={3}, journal={IEEE Transactions on Speech and Audio Processing}, author={Haeb-Umbach, Reinhold}, year={2001}, pages={299–302} }","mla":"Haeb-Umbach, Reinhold. “Automatic Generation of Phonetic Regression Class Trees for MLLR Adaptation.” <i>IEEE Transactions on Speech and Audio Processing</i>, vol. 9, no. 3, 2001, pp. 299–302, doi:<a href=\"https://doi.org/10.1109/89.906003\">10.1109/89.906003</a>.","chicago":"Haeb-Umbach, Reinhold. “Automatic Generation of Phonetic Regression Class Trees for MLLR Adaptation.” <i>IEEE Transactions on Speech and Audio Processing</i> 9, no. 3 (2001): 299–302. <a href=\"https://doi.org/10.1109/89.906003\">https://doi.org/10.1109/89.906003</a>.","short":"R. Haeb-Umbach, IEEE Transactions on Speech and Audio Processing 9 (2001) 299–302.","apa":"Haeb-Umbach, R. (2001). Automatic generation of phonetic regression class trees for MLLR adaptation. <i>IEEE Transactions on Speech and Audio Processing</i>, <i>9</i>(3), 299–302. <a href=\"https://doi.org/10.1109/89.906003\">https://doi.org/10.1109/89.906003</a>","ieee":"R. Haeb-Umbach, “Automatic generation of phonetic regression class trees for MLLR adaptation,” <i>IEEE Transactions on Speech and Audio Processing</i>, vol. 9, no. 3, pp. 299–302, 2001."},"oa":"1","status":"public","user_id":"44006","volume":9,"page":"299-302","_id":"11778","abstract":[{"lang":"eng","text":"In this paper, it is shown that a correlation criterion is the appropriate criterion for bottom-up clustering to obtain broad phonetic class regression trees for maximum likelihood linear regression (MLLR)-based speaker adaptation. The correlation structure among speech units is estimated on the speaker-independent training data. In adaptation experiments the tree outperformed a regression tree obtained from clustering according to closeness in acoustic space and achieved results comparable with those of a manually designed broad phonetic class tree"}],"publication":"IEEE Transactions on Speech and Audio Processing","issue":"3","keyword":["acoustic space","adaptation experiments","automatic generation","bottom-up clustering","broad phonetic class regression trees","correlation criterion","correlation methods","maximum likelihood estimation","maximum likelihood linear regression based speaker adaptation","MLLR adaptation","pattern clustering","phonetic regression class trees","speaker-independent training data","speech recognition","speech units","statistical analysis","trees (mathematics)"],"type":"journal_article","department":[{"_id":"54"}],"date_created":"2019-07-12T05:28:04Z","date_updated":"2022-01-06T06:51:08Z","intvolume":"         9","year":"2001","title":"Automatic generation of phonetic regression class trees for MLLR adaptation","author":[{"full_name":"Haeb-Umbach, Reinhold","last_name":"Haeb-Umbach","first_name":"Reinhold","id":"242"}],"doi":"10.1109/89.906003","main_file_link":[{"open_access":"1","url":"https://groups.uni-paderborn.de/nt/pubs/2001/Ha01.pdf"}],"language":[{"iso":"eng"}]},{"date_updated":"2022-01-06T06:51:11Z","intvolume":"         2","title":"LDA derived cepstral trajectory filters in adverse environmental conditions","year":"2000","author":[{"full_name":"Lieb, M.","first_name":"M.","last_name":"Lieb"},{"id":"242","last_name":"Haeb-Umbach","first_name":"Reinhold","full_name":"Haeb-Umbach, Reinhold"}],"doi":"10.1109/ICASSP.2000.859157","main_file_link":[{"url":"https://groups.uni-paderborn.de/nt/pubs/2000/LiHa00.pdf","open_access":"1"}],"language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"Amongst several data driven approaches for designing filters for the time sequence of spectral parameters, the linear discriminant analysis (LDA) based method has been proposed for automatic speech recognition. Here we apply LDA-based filter design to cepstral features, which better match the inherent assumption of this method that feature vector components are uncorrelated. Extensive recognition experiments have been conducted both on the standard TIMIT phone recognition task and on a proprietary 130-words command word task under various adverse environmental conditions, including reverberant data with real-life room impulse responses and data processed by acoustic echo cancellation algorithms. Significant error rate reductions have been achieved when applying the novel long-range feature filters compared to standard approaches employing cepstral mean normalization and delta and delta-delta features, in particular when facing acoustic echo cancellation scenarios and room reverberation. For example, the phone accuracy on reverberated TIMIT data could be increased from 50.7\\% to 56.0\\%"}],"publication":"IEEE International Conference on Acoustics, Speech, and Signal Processing (ICASSP 2000)","keyword":["acoustic echo cancellation algorithms","adverse environmental conditions","automatic speech recognition","cepstral analysis","cepstral features","cepstral mean normalization","command word task","delta-delta features","delta features","echo suppression","error rate reductions","feature vector components","FIR filters","LDA derived cepstral trajectory filters","linear discriminant analysis","long-range feature filters","phone accuracy","real-life room impulse responses","reverberant data","spectral parameters","speech recognition","standard TIMIT phone recognition task"],"type":"conference","department":[{"_id":"54"}],"date_created":"2019-07-12T05:29:50Z","status":"public","user_id":"44006","volume":2,"page":"II1105-II1108 vol.2","_id":"11869","citation":{"short":"M. Lieb, R. Haeb-Umbach, in: IEEE International Conference on Acoustics, Speech, and Signal Processing (ICASSP 2000), 2000, pp. II1105-II1108 vol.2.","chicago":"Lieb, M., and Reinhold Haeb-Umbach. “LDA Derived Cepstral Trajectory Filters in Adverse Environmental Conditions.” In <i>IEEE International Conference on Acoustics, Speech, and Signal Processing (ICASSP 2000)</i>, 2:II1105-II1108 vol.2, 2000. <a href=\"https://doi.org/10.1109/ICASSP.2000.859157\">https://doi.org/10.1109/ICASSP.2000.859157</a>.","ieee":"M. Lieb and R. Haeb-Umbach, “LDA derived cepstral trajectory filters in adverse environmental conditions,” in <i>IEEE International Conference on Acoustics, Speech, and Signal Processing (ICASSP 2000)</i>, 2000, vol. 2, pp. II1105-II1108 vol.2.","apa":"Lieb, M., &#38; Haeb-Umbach, R. (2000). LDA derived cepstral trajectory filters in adverse environmental conditions. In <i>IEEE International Conference on Acoustics, Speech, and Signal Processing (ICASSP 2000)</i> (Vol. 2, pp. II1105-II1108 vol.2). <a href=\"https://doi.org/10.1109/ICASSP.2000.859157\">https://doi.org/10.1109/ICASSP.2000.859157</a>","bibtex":"@inproceedings{Lieb_Haeb-Umbach_2000, title={LDA derived cepstral trajectory filters in adverse environmental conditions}, volume={2}, DOI={<a href=\"https://doi.org/10.1109/ICASSP.2000.859157\">10.1109/ICASSP.2000.859157</a>}, booktitle={IEEE International Conference on Acoustics, Speech, and Signal Processing (ICASSP 2000)}, author={Lieb, M. and Haeb-Umbach, Reinhold}, year={2000}, pages={II1105-II1108 vol.2} }","ama":"Lieb M, Haeb-Umbach R. LDA derived cepstral trajectory filters in adverse environmental conditions. In: <i>IEEE International Conference on Acoustics, Speech, and Signal Processing (ICASSP 2000)</i>. Vol 2. ; 2000:II1105-II1108 vol.2. doi:<a href=\"https://doi.org/10.1109/ICASSP.2000.859157\">10.1109/ICASSP.2000.859157</a>","mla":"Lieb, M., and Reinhold Haeb-Umbach. “LDA Derived Cepstral Trajectory Filters in Adverse Environmental Conditions.” <i>IEEE International Conference on Acoustics, Speech, and Signal Processing (ICASSP 2000)</i>, vol. 2, 2000, pp. II1105-II1108 vol.2, doi:<a href=\"https://doi.org/10.1109/ICASSP.2000.859157\">10.1109/ICASSP.2000.859157</a>."},"oa":"1"}]